Proof for $∃xA⇔¬∀x¬A$ I want to prove, that $∃xA⇔¬∀x¬A$, using classic axioms. I think, I have to start with the following step:
$∃xA⇔∃x¬¬A$
But I do not know, how to make this step, using axioms:
$∃x¬¬A⇔¬∀x¬A$
 A: It is quite easy with Natural Deduction.

(i) $∃xA(x) \rightarrow ¬∀x¬A(x)$

(1) $∀x¬A(x)$ --- assumed [a]
(2) $¬A(x)$ --- from (1) by $\forall$-E
(3) $∃xA(x)$ --- assumed [b]
(4) $A(x)$ --- assumed [c] for $\exists$-E
(5) $\bot$ --- from (4) and (2) by $\rightarrow$-E
(6) $\bot$ --- from (3), (4) and (5) by $\exists$-E, discharging [c]
(7) $¬∀x¬A(x)$ --- from (1) and (7) by $\rightarrow$-I, discharging [a]


(8) $∃xA(x) \rightarrow ¬∀x¬A(x)$ --- from (3) and (7) by $\rightarrow$-I, discharging [b]




(ii) $¬∀x¬A(x) \rightarrow ∃xA(x)$

(1) $¬∃xA(x)$ --- assumed [a]
(2) $A(x)$ --- assumed [b]
(3) $∃xA(x)$ --- from (2) by $\exists$-I
(4) $\bot$ --- from (1) and (3) by $\rightarrow$-E
(5) $¬A(x)$ --- from (2) and (4) by $\rightarrow$-I, discharging [b]
(6) $∀x¬A(x)$ --- from (5) by $\forall$-I
(7) $¬∀x¬A(x)$ --- assumed [c]
(8) $\bot$ --- from (6) and (7) by $\rightarrow$-E
(9) $∃xA(x)$ --- from (1) and (8) by Double Negation, discharging [a]


(10) $¬∀x¬A(x) \rightarrow ∃xA(x)$ --- from (7) and (9) by $\rightarrow$-I, discharging [c]


