Proof for $\forall x A(x) \Leftrightarrow \neg \exists x \neg A(x)$ I try to proof, that $\forall x A(x) \Leftrightarrow \neg \exists x \neg A(x)$
I know how to prove, that $\forall x A(x) \Rightarrow \exists xA(x)$, but I don't understand how to get negation.
 A: $$\forall x A(x) \equiv \forall x \lnot\lnot A(x) \equiv \lnot \exists x \lnot A(x)$$  
Perhaps it makes more sense to you if we start from the right, and move to the left. 
You'll need to remember that $$\lnot \forall x P(x) \equiv \exists x \lnot P(x)$$ and $$ \lnot \exists x P(x) \equiv \forall x \lnot P(x)$$
A: A proof by words. 
$\forall x A(X) \implies \lnot(\exists x \lnot A(x))$
$\forall x A(x)$ means that for every $x$ in the domain, the proposition $A(x)$ is true. This means that no $x$ exists such that $A(x)$ is false. Which can be written $\lnot (\exists x \lnot A(X))$, because the statement $\exists x \lnot A(X)$ always evaluates as false.
$\lnot(\exists x \lnot A(x)) \implies \forall x A(X)$
There is no $x$ such that $A(x)$ is false. Therefore on the domain of $x$, all $x$ imply $A(x)$ is true.
Small addendum: I think $\lnot(\exists x \lnot A(x))\equiv (\lnot\exists) x \lnot A(x)$.
A: Assuming one can use conversion of quantifiers (CQ) the following would be a way to show the biconditional using a Fitch-style proof checker. 

See Chapter 34 in the forallx text for conversion of quantifiers. Two of these conversion rules are derived in Chapter 36.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
