I have a doubt to prove by natural deduction of this:
$\vdash\forall x \forall y \varphi (x,y) \rightarrow \forall x \varphi(x,x)$
First of all, I took $\vdash\forall x \forall y \varphi (x,y)$ as a hipothesis
And eliminate $\forall y$, to deduce: $\forall x \varphi(x,x)$.
My question is: May I change y by x in this deduction?
Yes, it is valid.
The tedious way is to eliminate both universals to the same arbitrary constant, then reintroduce a universal from that.
$$\begin{array}{l|l:l} \hdashline \quad 1. & \forall x \forall y\; \varphi (x,y) & \textsf{Assume} \\ \hdashline \qquad 2. & \forall y\;\varphi (c, y) & 1, \forall\mathsf{E}\mid^x_c \\ \qquad 3. & \varphi (c,c) & 2, \forall\mathsf{E}\mid^y_c \\ \hline \quad 4. & \forall x\;\varphi(x,x) & 3, \forall\mathsf{I}\mid^c_x \\ \hline 5. & \big(\forall x \forall y\; \varphi (x,y)\big) \to \big(\forall x\;\varphi(x,x) \big) & 1,4, \to\mathsf{I} \end{array}$$
However, eliminating the universal $y$ to the bound variable $x$ is a valid short cut.