Theorem 2eu4
This theorem provides us with a definition of double existential
uniqueness ("exactly one \( x \) and exactly one \( y \) "). Naively one
might think (incorrectly) that it could be defined by \( \exists{!} x \, \exists{!} y \, \varphi \).
See 2eu1 for a condition under which the naive definition holds and
2exeu for a one-way implication. See 2eu5 and 2eu8 for alternate
definitions. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf
Lammen, 14-Sep-2019.)
Conclusion
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
Proof
l0
df-eu
l1
df-eu
\( \vdash \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists y \, \exists x \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \)
excom
\( \vdash \exists y \, \exists x \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \)
bianbi l1 _
l4
anbi12i l0 _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \wedge (\exists x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi) \)
l5
anandi
\( \vdash \exists x \, \exists y \, \varphi \wedge (\exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \wedge (\exists x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi) \)
2mo2
anbi2i _
\( \vdash \exists x \, \exists y \, \varphi \wedge (\exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi) \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
3bitr2i l4 l5 _