Predicate logic question Let $P$ be a $2$-ary predicate.   Is it true that 
$$\forall x, y P(x, y)$$
is equivalent to 
$$\forall x, y P(x, y) \wedge P(y, x)$$
This seems obviously true, but how do you formally prove it?
 A: Hint: Suppose it is true that:

$$
\forall x,y,~~P(x,y) \iff \boxed{\forall a,b,~~P(a,b)}
$$

Then by letting $a:=x$ and $b:=y$, we know that:
$$
\boxed{\forall x,y,~~P(x,y)}
$$
Likewise, by letting $a:=y$ and $b:=x$, we know that:
$$
\forall y,x,~~P(y,x) \iff \boxed{\forall x,y,~~P(y,x)}
$$
Hence, it follows that:

$$
\forall x,y,~~[P(x,y) \land P(y,x)]
$$

A: From
$$\tag0\forall x\forall y P(x,y)$$
by specialization (with $u$ being a "new/unused" variable)
$$\forall y P(u,y)$$
and by specialization again
$$P(u,x)$$
hence by generalization 
$$\forall u P(u,x)$$
and by another specialization
$$\tag1P(y,x).$$
Also, by specialization from $(0)$
$$\forall yP(x,y)$$
and by another specialization 
$$\tag2 P(x,y).$$
Now from $(1)$ and $(2)$ by conjunction
$$P(x,y)\land P(y,x)$$
and by generalization
$$\forall y (P(x,y)\land P(y,x))$$
and finally
$$\forall x\forall y( P(x,y)\land P(y,x)).$$
So far we have
$$\forall x\forall y P(x,y)\vdash \forall x\forall y (P(x,y)\land P(y,x))$$
hence by the deduction theorem
$$(3)\forall x\forall y P(x,y)\rightarrow \forall x\forall y (P(x,y)\land P(y,x)).$$

For the other direction, from
$$\forall x\forall y( P(x,y)\land P(y,x))$$
by specialization
$$\forall y( P(x,y)\land P(y,x))$$
and then 
$$ P(x,y)\land P(y,x)$$
and by conjunction elimination
$$ P(x,y)$$
and by generalization again
$$\forall y P(x,y)$$
and finally
$$\forall x\forall y P(x,y).$$
Thus
$$ \forall x\forall y (P(x,y)\land P(y,x))\vdash \forall x\forall y P(x,y)$$
and by the deduction theorem
$$\tag4 \forall x\forall y (P(x,y)\land P(y,x))\rightarrow \forall x\forall y P(x,y).$$
From $(3)$ and $(4)$ we have by biconditional introduction
$$ \forall x\forall y P(x,y)\leftrightarrow \forall x\forall y (P(x,y)\land P(y,x))$$
as desired.
A: Hint: I always like to explicitly specify a domain of quantification. IMHO, this makes for a more intuitive and "math-like" proof. So, with $U$ as the domain of quantification, the problem becomes to prove:
$\forall x,y (x,y\in U \to P(x,y))\leftrightarrow \forall x,y (x,y\in U \to P(x,y)\wedge P(y,x))$
(Some philosophy instructors may take exception to introducing set theoretic notation like this. Too "math-like".)
For '$\to$':
Assume $\forall x,y (x,y\in U \to P(x,y))$. Assume $a,b\in U$. Then obtain both $P(a,b)$ and $P(b,a)$, and generalize as required.
For '$\leftarrow$':
Assume $\forall x,y (x,y\in U \to P(x,y)\wedge P(y,x))$.  Assume $a,b\in U$. Then obtain $P(a,b)$, and generalize as required.
