How to better understand " x occurs free in a wff " in first order logic? On page 121 of Herbert Enderton's A Mathematical Introduction to Logic, the author gives a proof of the following example :
If x does not occur free in $\alpha$, then
$$
\vdash ( \alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha\rightarrow\beta)
$$

To prove this, it suffices to show that
    $$ 
\vdash  ( \alpha \rightarrow \forall x \beta) \rightarrow\forall x(\alpha\rightarrow\beta)
  $$
  and
    $$ 
\vdash  ( \alpha \rightarrow \forall x \beta) \leftarrow \forall x(\alpha\rightarrow\beta)
  $$
For the first case, it suffices to show that ( by the deduction and generalization theorem )
  $$
\{(\alpha \rightarrow \beta),\alpha\}\vdash\beta
$$
  But this is easy, since $\forall x \beta \rightarrow \beta $ is an axiom.

I try to verify that.
Step 1, By Deduction Theorem,
$$
( \alpha \rightarrow \forall x \beta) \vdash \forall x(\alpha\rightarrow\beta)
$$
Step 2, By Generalization Theorem,
$$
( \alpha \rightarrow \forall x \beta) \vdash \alpha\rightarrow\beta
$$
Step 3, By Deduction Theorem,
$$
\{(\alpha \rightarrow \beta),\alpha\}\vdash\beta
$$
What baffle me :


*

*Is Step 2 plausible?  We don't know if $\beta$ is free or not...

*Given an axiom of Enderton's system : 

$  \forall x \alpha \rightarrow \alpha_{x}^{t} $
  , where $t$ is substitutable for $x$ in $\alpha$ 

, how can I make sense of   $\forall x \beta \rightarrow \beta $ ?
I ask this question mainly because I'm deeply baffled with the idea of " variable occurs free ".  Can anyone translate $\vdash ( \alpha \rightarrow \forall x \beta) \leftrightarrow \forall x(\alpha\rightarrow\beta)$ into Englsih ( or give an simple algebra example ) and compare the two cases where $\alpha $ occurs free and not occurs free?  I believe it will help me understand why Enderton's proof is plausible.
Thank you ( :
 A: For :


$\vdash (α→∀xβ)→∀x(α→β)$


the proof is :
1) $(α→∀xβ)$ --- assumed
2) $\alpha$ --- assumed
3) $∀xβ$ --- by modus ponens
4) $\beta$ --- from 3) by Ax.2 : $∀x \varphi→\varphi^x_t$, where $t$ is substitutable for $x$ in $\varphi$; we apply it with $\beta$ as $\varphi$ and $x$ as $t$.
5) $\alpha \rightarrow \beta$ --- from 2) and 4) by Deduction Th
6) $\forall x (\alpha \rightarrow \beta)$ --- from 5) by GENERALIZATION THEOREM [page 117] : If  $\Gamma \vdash \varphi$ and $x$ do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \varphi$.
In this step, $\Gamma = \{ α→∀xβ \}$; thus in order to apply Gen Th, we have to satisfy the proviso : $x$ not free in it. This requires that $x \notin FV(\alpha)$.
The theorem follows applying Deduction Th to 1)-6):


$\vdash (α→∀xβ)→∀x(α→β)$.



For :


$\vdash ∀x(α→β) \rightarrow (α→∀xβ)$


the proof is :
1) $∀x(α→β)$ --- assumed
2) $α→β$ from 1) by Ax.2, with $α→β$ as $\varphi$ and $x$ as $t$.
3) $\alpha$ --- assumed
4) $\beta$ --- by modus ponens
5) $\forall x \beta$ --- from 4) by GENERALIZATION THEOREM. In this step, $\Gamma = \{ ∀x(α→β), α \}$; thus, in order to apply it, we need : $x \notin FV(\alpha$)
6) $\alpha \rightarrow \forall x \beta$ --- from 3)-5) by Deduction Th.
The theorem follows applying Deduction Th to 1)-6):


$\vdash ∀x(α→β) \rightarrow (α→∀xβ)$.




Why we need the proviso ?
Consider :

$(x = 0) \rightarrow (x = 0)$

it is a (first-order) instance of the tautology $A \rightarrow A$; thus, by Ax.1, its generalization :

$\forall x((x = 0) \rightarrow (x = 0))$

is an axiom of first-order logic, and thus a valid formula.
Consider now :

$(x = 0) \rightarrow \forall x (x = 0)$;

if we "forget" the proviso, this formula is equivalent to previous one; thus it must be valid.
But it is not; to show it, we apply modus ponens to get :

$(x = 0) \vDash \forall x (x = 0)$.

Consider the definition [page 88] of Logical Implication :

Let $\Gamma$ be a set of wffs, $\varphi$ a wff. Then $\Gamma$ logically implies $\varphi$, written $\Gamma \vDash \varphi$, iff for every structure $\mathfrak A$ for the language and every function $s : Var \to |\mathfrak A|$ such that $\mathfrak A$ satisfies every member of $\Gamma$ with $s$, $\mathfrak A$ also satisfies $\varphi$ with $s$.

and consider the function $s$ such that $s(x)=0$.
With $|\mathfrak A| = \mathbb N$ and this $s$, we have that $(x = 0)$ is satisfied, while of course $\forall x (x = 0)$ is not (it is obviously false that all natural numbers are equal to $0$).

Consider now the example :

$(0=0) \rightarrow \forall x (x=0)$;

in this case the proviso is satisfied; thus, it must be equivalent to :

$\forall x ((0=0) \rightarrow (x=0))$.

This is verified in $\mathbb N$, where the two are both false.
