Show that $∀x∀yPxy⊢∀y∀xPyx$ using the Generalization theorem Show that $∀x∀yPxy⊢∀y∀xPyx$. > By the Generalization Theorem, it is sufficient to show that $∀x∀yPxy⊢Pyx$. By EAV, $∀x∀yPxy⊢∀x∀zPxz$. By axiom group 2, $⊢∀x∀zPxz→∀zPyz$ and $⊢∀zPyz→Pyx$. By applying MP twice, we get $∀x∀yPxy⊢Pyx$. From above, Existence of Alphabetic Variants theorem applied in the second line, I cannot understand it well. Applying Axiom groups or MP are not difficult but I cannot figure out why EAV used in the second line. \---edit I understand that $\text{y is not substitutable for x in $\forall yPxy$}$ So, using Alphabetic Variants y to z then $\text {z is substitutable for x in $\forall yPxy$}?$

Yes: EAV simply amounts to the equivalence between $\forall x P(x)$ and $\forall yP(y)$.

That is, provided that we avoid "clashing" of variables, the choice of the bound variable does not affect the meaning of a formula.

In the proof above it is needed in order to "free" $y$ prior to "swap" it with $x$.

As you said, we choose a new variable $z$ that does not occur into $Pxy$; thus, for sure it is _substitutable for_ $x$ in $∀x∀yPxy$.