Theorem 2euexv
Double quantification with existential uniqueness. Version of 2euex
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 \rightarrow \exists y \, \exists{!} x \, \varphi \)
Proof
l0
df-eu
\( \vdash \exists{!} x \, \exists y \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \)
l1
excom
\( \vdash \exists x \, \exists y \, \varphi \leftrightarrow \exists y \, \exists x \, \varphi \)
nfe1
l3
nfmov _
19.8a
l5
moimi _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \exists^\ast x \, \varphi \)
moeu
\( \vdash \exists^\ast x \, \varphi \leftrightarrow \exists x \, \varphi \rightarrow \exists{!} x \, \varphi \)
sylib l5 _
eximd l3 _
\( \vdash \exists^\ast x \, \exists y \, \varphi \rightarrow \exists y \, \exists x \, \varphi \rightarrow \exists y \, \exists{!} x \, \varphi \)
biimtrid l1 _
impcom _
\( \vdash \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \rightarrow \exists y \, \exists{!} x \, \varphi \)
sylbi l0 _