Theorem 2exeuv
Double existential uniqueness implies double unique existential
quantification. Version of 2exeu with \( x \) and \( y \) distinct, but
not requiring [ax-13]. (Contributed by NM, 3-Dec-2001.) (Revised by
Wolf Lammen, 2-Oct-2023.)
Conclusion
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \rightarrow \exists{!} x \, \exists{!} y \, \varphi \)
Proof
l0
eumo
\( \vdash \exists{!} x \, \exists y \, \varphi \rightarrow \exists^\ast x \, \exists y \, \varphi \)
euex
moimi _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast x \, \exists{!} y \, \varphi \)
l3
syl l0 _
2euexv
l5
anim12ci l3 _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \rightarrow \exists x \, \exists{!} y \, \varphi \wedge \exists^\ast x \, \exists{!} y \, \varphi \)
df-eu
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \leftrightarrow \exists x \, \exists{!} y \, \varphi \wedge \exists^\ast x \, \exists{!} y \, \varphi \)
sylibr l5 _