Addressing question 1 specifically:
I am not an expert in the subject but I took a couple of logic subjects at uni and never really saw a standard naming convention for the deduction rules in first order logic. You are likely to find different authors with different conventions. What is most important is you follow the rules correctly and you have in this case.
One of the reasons is that the Generalization Theorem [see page 117] used in the last step of the proof is not a rule of the calculus, but a so-called meta-theorem.
It is a theorem about $\vdash$, i.e. the derivability relation, and $\vdash$ is not part of the syntax of the calculus [see page 69].
The theorem asserts that (under certain circumstances) a derivation in the calculus exists, but it is not itself a derivation in the calculus.
We can convert the proof provided at page 122 into a "fully formal" derivation following the steps in the proof of the Gen Th, inserting the "missing" steps.
Example : how to remove the first use of Gen Th in step 4 ? We have to use the Case 3 of the proof of the meta-theorem.
In your expanded proof we have to use the universal closure of step 3) :
3a) $\forall x (x=x → (x=y → y=x))$
as well as that of Ax.5 :
4a) $\forall x (x=x).$
Thus :
4b) $\forall x (x=x → (x=y → y=x)) \to (\forall x (x=x) → \forall x (x=y → y=x))$ --- Ax.3
4c) $\forall x (x=x) → \forall x (x=y → y=x))$ --- from 3a) and 4b) by MP
4d) $\forall x (x=y → y=x)$ --- from 4a) and 4c) by MP.
The same procedure must then be used to derive 3a) above from Ax.6 and the universal closure of step 2 (see page 112 : "The logical axioms are then all generalizations of wffs of the following forms [...] : 1. Tautologies; [...]").
In the same way, for the 2nd use of Gen Th.
The same for Rule T [page 118] used in step 3: you have already provided the "elimination" of it inserting into the proof the corresponding elementary propositional steps.
Best Answer
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.