Are these logic statements equivalent?

Question

I understand logical statements #1 and #2 to be equivalent. I have been told that logical statement #3 is not equivalent to #2, but I do not understand how or why (assuming what I have been told is correct). The domain of variables x and y is the same.

1. $\forall{x}.(P(x) \iff Q(x))$
2. $\forall{x}.((P(x) \to Q(x)) \wedge (Q(x) \to P(x)))$
3. $\forall{x, y}.((P(x) \to Q(x)) \wedge (Q(y) \to P(y)))$

Answer 1

I refuse to believe that #2 and #3 are not equivalent on the grounds that the explicit names of quantified variables don't matter, just that they are distinct from each other, e.g. for all univariate predicates $P$ we have that $\forall x. P(x) \iff \forall y. P(y)$.

Here is an attempt to be as explicit as possible with a proof that they are equivalent (forgive me if it has a mistake, it has been a while since I've tried to write anything about predicate calculus):

First, universal quantifiers distribute over conjunctions, so: $$ \forall{x}.((P(x) \to Q(x)) \wedge (Q(x) \to P(x))) \iff (\forall{x}.(P(x) \to Q(x))) \wedge (\forall{x}.(Q(x) \to P(x))) $$

Second, conjunctive elimination will give us each half independently. Third, variable names don't matter so write $\forall{x}.(Q(x) \to P(x))$ as $\forall{y}.(Q(y) \to P(y))$. Fourth, conjunctive introduction gives us the following: $$ (\forall{x}.(P(x) \to Q(x)))\wedge (\forall{y}.(Q(y) \to P(y))) $$ Finally, universal introduction of the other variable to each side, and factoring the quantifiers out of the conjunction, shows that #2 implies #3.

Now do something similar the other way around. Point being that this is obviously true, and only a sadist would make you prove it.