I need to check if my proof for $\vdash_\Sigma ((\forall x_1 (\forall x_2 p(x_1, x_2))) \implies p(f(x_1, x_2), x_2))$ is correct for $x_1,x_2 \in X$, $f(x_1,x_2) \in T_\Sigma$ and $p \in P_2$.
Def(Ax4): $(\forall x \varphi) \implies [\varphi]{_t}^x$ if $t \triangleright_\Sigma x : \varphi$
Def(Gen): $\varphi \vdash_\Sigma \forall x \varphi$
Consider the derivation sequence for $(\forall x_1 (\forall x_2 p(x_1, x_2))) \vdash_\Sigma p(f(x_1, x_2), x_2)$:
1.$(\forall x_1 (\forall x_2 p(x_1, x_2)))$ (Hip)
2.$(\forall x_2 p(x_1, x_2))$ (Ax4 + ModusPonens-1) ($x_1 \triangleright_\Sigma x_1 : (\forall x_2 p(x_1, x_2))$
3.$p(x_1,x_2)$ (Ax4 + ModusPonens-2) $(x_2 \triangleright_\Sigma x_2 : p(x_1, x_2))$
4.$(\forall x_1 p(x_1, x_2))$ (Gen-3)
5.$p(f(x_1,x_2),x_2)$(Ax4 + ModusPonens-4) $(f(x_1,x_2) \triangleright_\Sigma x_1 : p(x_1, x_2))$.
Because $(\forall x_1 (\forall x_2 p(x_1, x_2)))$ is a closed formula then the generalization in step 4 is not essential therefore one can use de Deduction Metatheorem to conclude: $$\vdash_\Sigma ((\forall x_1 (\forall x_2 p(x_1, x_2))) \implies p(f(x_1, x_2), x_2))$$.
Is my proof correct, that is, are all the applications of Ax4 are valid and also the application of the Deduction Metatheorem is also valid? Thanks in advance.