Confusion regarding $\models \forall x A \equiv \forall y A[y/x]$

Question

I have some confusion regarding the following statement given in Jean H. Gallier's book "Logic for Computer Science". It says,

For every formula $A$ $$\models \forall x A \equiv \forall y A[y/x]$$

Now if I take $A = \forall y \Phi(x,y)$, then $A[y/x] = \Phi(y,y)$. Hence using above statement I have $$\models \forall x \forall y \Phi(x,y) \equiv \forall y \forall y \Phi(y,y)$$ Which is just $$\models \forall x \forall y \Phi(x,y) \equiv \forall y \Phi(y,y)$$ And this statement is definitely wrong. Is this because I am using a bounded variable to substitute a free variable ? My end goal was to actually prove the following, $$\forall x \forall y \Phi(x,y) \rightarrow \forall y \Phi(y,y) $$ How do I prove this ?

---

Here is the proof from tree proof generator https://www.umsu.de/trees/#%E2%88%80x%E2%88%80yF(x,y)%E2%86%92%E2%88%80yF(y,y)

---

But a better proof will be much appreciated.

Answer 1

If $A = ∀yΦ(x,y)$ , then $A[y/x]=A$ because $y$ is not free for $x$ in $A$.

The proof must be:

1) $∀x∀yΦ(x,y)$,

2) $∀yΦ(z,y)$ by Universal Instantiation,

3) $Φ(z,z)$ by UI,

and finally:

$∀yΦ(y,y)$ by Universal Generalization.

But the last formula is not equivalent to the first one: consider $\forall y (y \le y)$, which is true in $\mathbb N$, and $\forall x \forall y (x \le y)$, which is not.

---

Regarding the title: 1) $\forall x A$, 2) $A[y/x]$, if $y$ is free for $x$ in $A$, 3) $\forall y A[y/x]$.