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$.