Theorem 2euex
Double quantification with existential uniqueness. Usage of this theorem
is discouraged because it depends on [ax-13]. Use the weaker 2euexv
when possible. (Contributed by NM, 3-Dec-2001.) (Proof shortened by
Andrew Salmon, 9-Jul-2011.) (New usage is discouraged.)
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
nfmo _
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 _