∀x(A→ B) ├ ¬∃x(A ∧ ¬B) prove with natural deduction

Question

Please help me prove the following $$∀x(A→ B) ├ ¬∃x(A ∧ ¬B)$$ using natural deduction.

This is what I have done so far:

1. $∀x(A→ B)$
2. $∃x(A ∧ ¬B)$ assumption
3. n $(A ∧ ¬B)[n/x]$ assumption
4. $A[n/x] ∧ ¬B[n/x]$
5. $A[n/x]$ $∧e,4$
6. $B[n/x]$ $∧e,4$

How should I continue?

Answer 1

1) $\forall x(A \rightarrow B)$ --- premise

2) $A \rightarrow B$ --- from 1) by $\forall$-elimintion

3) $\exists x (A \land \lnot B)$ --- assumed [a]

4) $A \land \lnot B$ --- assumed [b] for $\exists$-elimination

5) $A$ --- from 4) by $\land$-elimination

6) $\lnot B$ --- from 4) by $\land$-elimination

7) $B$ --- from 5) and 2) by $\rightarrow$-elimination

8) $\bot$ --- from 6) and 7) by $\rightarrow$-elimination ($\lnot B$ is an abbreviation for : $B \rightarrow \bot$)

9) $\bot$ --- from 3), 4)-8) by $\exists$-elimination, discharging assumption [b]

10) $\lnot \exists x (A \land \lnot B)$ --- from 3) and 9) by $\rightarrow$-introduction, discharging assumption [a].

Answer 2

$$\def\fitch#1#2{~~~\begin{array}{|l} #1\\\hline #2\end{array}}\fitch{~~1.~~\forall x~(A\to B)}{\fitch{~~2.~~\exists x~(A\land\lnot B)}{\fitch{\hspace{-4ex}\boxed n~~~~3.~~(A\land\lnot B)[n/x]}{~~4.~~A[n/x]\;\land\lnot B[n/x]\\~~5.~~A[n/x]\hspace{15ex}{\land}\mathsf e~4\\~~6.~~\lnot B[n/x]\hspace{13.5ex}{\land}\mathsf e~4\\[1ex]~~7.~~(A\to B)[n/x]\hspace{8ex}\forall\mathsf e~1\\~~8.~A[n/x]\to B[n/x]\\~~9.~~B[n/x]\hspace{15ex}{\to}\mathsf e~8,5\\10.~~\bot\hspace{20ex}\lnot\mathsf e~9,6}\\11.~~\bot\hspace{23ex}\exists\mathsf e~2,3{-}10}\\12.~~\lnot\exists x~(A\land\lnot B)\hspace{13.5ex}\lnot\mathsf i~2{-}11}$$