How to show that $\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$? 
Assume $x$ doesn't occur free in $\alpha$, show that: $$\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$$

This is an exercise on page 130, A Mathematical Introduction to Logic, Herbert B. Enderton（2ed). 
Here's my attempt: For the '$\to$' direction, since $x$ doesn't occur free in $\alpha$, we have $α→∀x α$ and $\forall x \alpha \to \alpha$ as logical axiom(In the second formula, we have$\alpha_x^x = \alpha$). Thus it suffice to show $\vdash (\forall x \beta \to \forall x \alpha) \rightarrow \exists x (\beta \to \alpha)$. By logical axiom $∀ x(α→β)→( ∀ x α→∀x β)$, it would suffice to show $\vdash \forall x (\beta \to   \alpha) \rightarrow (\exists x (\beta \to \alpha))$. It has been shown in a previous exercise that there's a deduction $∀ x ϕ→∃x ϕ$, so we are done for the "$\to$" part.
The problem for me is how to show the "$\leftarrow$" direction.
Added: Here's logical axioms that we can employ: 

  
*
  
*Tautologies(in the sense of propositional logic);
  
*$∀ x α →α^x_
t $, where $t$ is substitutable for $x$ in $α$ ($α^x_
t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
  
*$∀ x(α→β)→( ∀ x α→∀x β)$;
  
*$α→∀x α$, where $x$ does not occur free in $α$.
  

Besides, generalization theorem and deduction principle can be utilized:

If $\Gamma \vdash ϕ$ and $x$ do not occur free in any
  formula in$\Gamma$, then$\Gamma \vdash ∀ x ϕ$.
If $\Gamma ; γ \vdash ϕ,$ then $\Gamma \vdash  γ \to ϕ$.

 A: 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)$.

A: As coffeemath has already observed, the interesting case is α being false.
In that situation the implication towards α is the same as negation, which means the direction from left-to-right is in fact just a variant of the de-Morgan law for quantifiers (the hard classical part of it).
Lets switch notation to that of the formal proof system Isabelle/Isar.  The proof of that part of de-Morgan then looks like this:
theorem de_Morgan_classical:
  assumes *: "¬ (∀x. B x)"
  shows "∃x. ¬ B x"
proof (rule classical)
  assume **: "¬ (∃x. ¬ B x)"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      then have "∃x. ¬ B x" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * show "∃x. ¬ B x" by contradiction
qed

You can read this is pseudo-code, but it is machine-checked natural deduction.  Note that in the formal language, dependence on some argument is explicit, as in B x, and just A means it cannot depend on hidden variables.
Instead of using that law in the proof, we re-use its proof to make a slightly more general version as follows:
lemma
  assumes *: "(∀x. B x) ⟶ A"
  shows "∃x. (B x ⟶ A)"
proof (rule classical)
  assume **: "¬ (∃x. (B x ⟶ A))"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      have "B x ⟶ A"
      proof
        assume "B x"
        with `¬ B x` show A ..
      qed
      then have "∃x. (B x ⟶ A)" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * have A ..
  fix a from `A` have "B a ⟶ A" ..
  then show "∃x. (B x ⟶ A)" ..
qed

The other direction is just plain natural deduction, without anything special.  There are no classical cases to be considered.
lemma
  assumes *: "∃x. (B x ⟶ A)"
  shows "(∀x. B x) ⟶ A"
proof
  assume **: "∀x. B x"
  from * obtain a where ***: "B a ⟶ A" ..
  from ** have "B a" ..
  with *** show A ..
qed

A: If $\alpha$ holds, both sides of the iff are true, since anything implies true. So suppose $\alpha$ is false. 
Now assume $\exists x (\beta \to \alpha)$. Then take $c$ as such an $x$, and get to $$\beta_c^x \to \alpha,$$ where we have used $\alpha_c^x=\alpha$, since $x$ is not free in $\alpha$. Since $\alpha$ is false, $\beta_c^x$ must be false, so that also $\forall x \beta$ is false, and from this $\forall x \beta \to \alpha$ follows.
I think the steps here are reversible, so that one could do the forward implication in a similar way. However the OP only asked about the reverse implication just treated. I used "existential instantiation" (which is what one text I used called it), which is not one of the rules cited in the OP, however I think it must be there somehow in any formal axiomitization.
