Having the OP's question already received answers, I submit this "long" comment aimed at providing a proof using Enderton's axioms and modus ponens, which is the only rule of inference (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).
We have to prove (Q3A) [see Exercise 8, page 130] :
$\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.
First part : $\leftarrow$
(1) $\forall x \beta$ --- assumed
(2) $\beta_c^x$ --- from (1) by Ax.2 and mp, where the constant symbol $c$ does not occur in $\alpha, \beta$
(3) $\beta_c^x \rightarrow \alpha$ --- assumed
(4) $\alpha$ --- from (2) and (3) by mp
By COROLLARY 24H (RULE EI) [page 124], having proved $\forall x \beta, \beta_c^x \rightarrow \alpha \vdash \alpha$, where $c$ does not occur in $\beta$ nor in $\alpha$ (because $x \notin FV(\alpha)$), we have :
(5) $\forall x \beta, \exists (\beta \rightarrow \alpha) \vdash \alpha$
(6) $\exists (\beta \rightarrow \alpha) \vdash (\forall x \beta \rightarrow \alpha)$ --- from (5) by DT.
Second part : $\rightarrow$
(1) $\lnot \beta \vdash \beta \rightarrow \alpha$ --- by $\vDash_{TAUT} \lnot \phi \rightarrow (\phi \rightarrow \psi)$, assuming $\lnot \beta$
(2) $\forall x \beta \rightarrow \alpha$ --- assumed
(3) $\lnot \exists x (\beta \rightarrow \alpha)$ --- assumed
(4) $\exists x (\beta \rightarrow \alpha)$ --- from (1) by the "derived rule" : $\varphi_t^x \rightarrow \exists x \varphi$ [provable from Ax.2] and mp
Thus we have : $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$, from (1) and (4) and $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \lnot \exists x (\beta \rightarrow \alpha)$, from (1) and (3); we apply : COROLLARY 24E (REDUCTIO AD ABSURDUM) [page 119] and $\vDash_{TAUT} \lnot \lnot \phi \rightarrow \phi$ and mp to conclude with :
(5) $\lnot \exists x (\beta \rightarrow \alpha) \vdash \beta$
(6) $\forall x \beta$ --- from (5) by GENERALIZATION THEOREM [page 117] ($x$ is not free in assumptions (2), because $x \notin FV(\alpha$), and (3) and assumption (1) has been "discharged" in (5))
(7) $\alpha$ --- from (2) and (6) by mp
(8) $\beta \rightarrow \alpha$ --- From (7) and $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$ and mp
(9) $\exists x(\beta \rightarrow \alpha)$ --- from (8) by the "derived rule" in (4) above
We apply again COROLLARY 24E (REDUCTIO AD ABSURDUM) with : $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \lnot \exists x (\beta \rightarrow \alpha)$, and $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \exists x (\beta \rightarrow \alpha)$, from (2)-(9), and Double Negation to conclude with :
(10) $(\forall x \beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$.
Addendum
We add as an exercise the proof in Enderton's system of (Q2B) [see Exercise 8, page 130] :
$\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$.
First part : $\rightarrow$
(I've "streamlined" a little bit the "tautological" steps)
(1) $\alpha \rightarrow \exists x \beta$ --- assumed
(2) $\forall x \lnot (\alpha \rightarrow \beta)$ --- assumed
(3) $\alpha \land \lnot \beta$ --- from (2) by Taut
(4) $\lnot \beta$ --- from (3) by Taut
(5) $\forall x \lnot \beta$ --- by the Generalization Theorem [page 117], because $x$ is not free in assumptions (1) and (2)
(6) $\lnot \exists x \beta$ --- abbreviation
(7) $\alpha$ --- from (3) by Taut
(8) $\exists x \beta$ --- from (1) by mp.
Having derived the contradiction [with (6) and (8)], we apply Corollary 24E (Reductio ad Absurdum) [page 119] : if $\Gamma \cup \{ \varphi \}$ is inconsistent, then $\Gamma \vdash \lnot \varphi$, with $\Gamma = \{ \alpha \rightarrow \exists x \beta \}$, and $\varphi := \forall x \lnot (\alpha \rightarrow \beta)$.
Thus we may conclude :
(9) $\lnot \forall x \lnot (\alpha \rightarrow \beta)$
that is : $\alpha \rightarrow \exists x \beta \vdash \exists x (\alpha \rightarrow \beta)$.
Finally :
(A) $\vdash (\alpha \rightarrow \exists x \beta) \rightarrow \exists x (\alpha \rightarrow \beta)$ --- by Deduction Theorem.
Second part : $\leftarrow$
(1) $\alpha \rightarrow \beta[x/c]$ --- assumed, where $c$ is an individual constant
(2) $\lnot \beta[x/c] \rightarrow \lnot \alpha$ --- by Taut
(3) $\forall x \lnot \beta$ --- assumed
(4) $\lnot \beta[x/c]$ --- from Ax.2 and (3) by mp
(5) $\lnot \alpha$ --- form (2) and (4) by mp
(6) $\forall x \lnot \beta \rightarrow \lnot \alpha$ --- form (3) and (5) by Deduction Theorem
(7) $\alpha \rightarrow \lnot \forall x \lnot \beta$ --- by Taut
(8) $\alpha \rightarrow \exists x \beta$ --- abbreviation.
Now we apply Corollary 24H (Rule EI) : assume that the constant symbol $c$ does not occur in $\varphi, \psi$ or $\Gamma$, and that $\Gamma \cup \{ \varphi[x/c] \} \vdash \psi$; then $\Gamma, \exists x \varphi \vdash \psi$, where $\Gamma = \emptyset$, $\varphi[x/c] := \alpha \rightarrow \beta[x/c]$ and $\psi := \alpha \rightarrow \exists x \beta$.
Thus we may conclude with :
$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.
Finally :
(B) $\vdash \exists x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \exists x \beta)$.
The theorem follows from (A) and (B).
2nd Addendum
For the second part : $\leftarrow$, we can prove it without Corollary 24H (Rule EI).
(1) $\exists x(\alpha \rightarrow \beta)$ --- assumed
(2) $\alpha$ --- assumed
(3) $\lnot \exists x \beta$ --- assumed
(4) $\lnot \lnot \forall x \lnot \beta$ --- abreviation for $\exists$
(5) $\forall x \lnot \beta$ --- by Taut
(6) $\lnot \beta$ --- Ax.2
(7) $\vDash_{TAUT} \alpha \rightarrow (\lnot \beta \rightarrow \lnot (\alpha \rightarrow \beta))$
(8) $\lnot (\alpha \rightarrow \beta)$ --- from (2), (6) and (7) by mp
(9) $\forall x \lnot (\alpha \rightarrow \beta)$ --- by Gen Th ($x \notin FV(\alpha)$)
(10) $\lnot \exists x (\alpha \rightarrow \beta)$ --- abbreviation
(11) $\lnot \lnot \exists x \beta$ --- we apply Corollary 24E (Reductio ad Absurdum) [page 119] to (3), with (1) and (10)
(12) $\exists x \beta$ --- by Taut
(13) $\alpha \rightarrow \exists x \beta$ --- from (2) by Deduction Theorem.
So again :
$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.
Best Answer
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) :
as well as that of Ax.5 :
Thus :
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.