Natural Deduction proof for $\forall x \neg A \implies \neg \exists xA$ $\forall x \neg A \implies \neg \exists xA$
I won't ask you to solve this for me, but can you please give some guiding lines on how to approach a proof in NDFOL?
There are many tricks that the TA shows in class, that I could not dream of...
P.S. I managed to proof $\neg \exists xA \implies \forall x \neg A$ but could not get on from there.
Thanks!

After the proposed answer, let me see if I got this correct:  


*

*$\exists x A \implies \exists x A$ (axiom assumption)

*$\exists x A \implies A$ (from 1)

*$\exists x A, \forall x \neg A \implies \forall x \neg A$ (axiom assumption)

*$\exists x A, \forall x \neg A \implies \neg A$ ($\forall$ extraction, from 3)

*$\forall x \neg A \implies \neg \exists x A$ (from 2,4)


Am I correct?
I could not understand the justification going from (1) to (2)
 A: To prove an implication, the general guideline for constructing formal proofs is: Assume the premise and the negation of the consequence, and derive a contradiction.
In your present case:

Assume $\exists x A(x)$. By Existential Instantiation, we have $A(t)$ for some (unspecified but fixed) $t$.
Assume $\forall x \neg A(x)$. By Universal Instantiation, we have $\neg A(t)$.
Now $A(t)$ and $\neg A(t)$ combine into a contradiction $\bot$.
We use Negation Introduction on the open assumption $\exists x A(x)$ to conclude $\neg \exists x A(x)$.
Finally, by Implication Introduction, we conclude the desired $\forall x \neg A(x) \implies \neg \exists x A(x)$ holds without any assumption.
Q.E.D.

Addressing OP's efforts:
As you see, there is a difference in our notations. I have parametrised $A$ as $A(x)$, while you haven't. However, this is crucial for the inference of $(2)$ from $(1)$. The expression $A(t)$ contains a $t$, which we can think of as an arbitrary "witness" of $\exists x A(x)$. It is this witness $t$ we apply Universal Instantiation / $\forall$ Extraction to: Since $\forall x \neg A(x)$, in particular $\neg A(t)$, where $t$ is the witness to $\exists x A(x)$.
This working with witnesses requires some practice, and even then one can sometimes mix things up. They are however crucial for the validity of the reasoning, so be sure to try and derive some more "trivialities" containing existential quantifiers!
A final remark (inspired by the comment by Peter Smith) is that in place of where you wrote "axiom", it's better to write one of "assumption" or "hypothesis", because these words have different meanings in mathematical lingo.
A: Stated in a slightly different way from LF...


*

*$\forall x \neg A(x)$  (Assume)

*$A(y)$  (Assume)

*$\neg A(y)$  (Universal Specification, line 1)

*$A(y) \wedge \neg A(y)$ (Join, lines 2, 3)

*$\neg\exists x A(x) $ (Conclusion, line 2)

*$\forall x \neg A(x) \rightarrow \neg\exists x A(x)$ (Conclusion, line 1)
