= Solution
Choose fresh arbitrary <eigenvariables> $u,v$. Under $u=v$, use the <equality elimination rule> to transport $P(u)$ to $P(v)$. For the reverse direction, first derive $v=u$ by the symmetry derivation above. In full <natural deduction> form:
$$
\begin{array}{rll}
1&[u=v]^a&\text{assumption}\\
2&\quad[P(u)]^b&\text{assumption}\\
3&\qquad P(v)&=E\ 1,2\\
4&\quad P(u)\to P(v)&\to I\ (2\text{--}3)\\
5&\quad u=u&=I\\
6&\quad v=u&=E\ 1,5\quad(\phi(w)\equiv w=u)\\
7&\quad[P(v)]^c&\text{assumption}\\
8&\qquad P(u)&=E\ 6,7\\
9&\quad P(v)\to P(u)&\to I\ (7\text{--}8)\\
10&\quad(P(u)\to P(v))\land(P(v)\to P(u))&\land I\ 4,9\\
11&u=v\to((P(u)\to P(v))\land(P(v)\to P(u)))&\to I\ (1\text{--}10)\\
12&\forall y\,(u=y\to((P(u)\to P(y))\land(P(y)\to P(u))))&\forall I\ 11\\
13&\forall x\forall y\,(x=y\to((P(x)\to P(y))\land(P(y)\to P(x))))&\forall I\ 12.
\end{array}
$$
All <temporary assumptions> are discharged before either <universal quantifier introduction rule> application, so both <eigenvariable conditions> hold. No premises remain:
$$
\boxed{\vdash\forall x\forall y\,(x=y\to((P(x)\to P(y))\land(P(y)\to P(x)))).}
$$
Back to article page
