Try to proof this using the definition of logic consequence.
$\forall x(\alpha \rightarrow \beta), \forall x \alpha \models \forall x \beta$
Let's say that: $\Gamma = \alpha \rightarrow \beta$, by definition of logic consequence: for all interpretation $\mathfrak{I}\models\Gamma$ must then $\mathfrak{I}\models\forall x \beta$.
Suppose any interpretation $\mathfrak{I}$ such that $\mathfrak{I}\models\Gamma$. With this i have that $\mathfrak{I}$ satisfy this two cases:
1) $\mathfrak{I}\models\forall x(\alpha \rightarrow \beta)$
By definition of relation of satisfaction of "$\forall$":
for all a $\in$ A, $\mathfrak{I}[a/x]\models(\alpha \rightarrow \beta)$
By definition of relation of satisfaction of "$\rightarrow$":
for all a $\in$ A, if $\mathfrak{I}[a/x]\models\alpha$ then $\mathfrak{I}[a/x]\models\beta$
2) $\mathfrak{I}\models\forall x \alpha$.
By definition of relation of satisfaction of "$\forall$":
for all a $\in$ A, $\mathfrak{I}[a/x]\models\alpha$
So, since there is a interpretation that satisfy 1) and this interpretation also satisfy 2). By Modus Ponens(1 and 2) we have:
for all a $\in$ A, $\mathfrak{I}[a/x]\models \beta$.
By definition of relation of satisfaction of "$\forall$" we have:
$\mathfrak{I}\models\forall x \beta$.
This proof is correct?
Yes, your proof looks correct.