Theorem 2euswap
A condition allowing to swap an existential quantifier and a unique
existential quantifier. Usage of this theorem is discouraged because it
depends on [ax-13]. Use the weaker 2euswapv when possible.
(Contributed by NM, 10-Apr-2004.) (New usage is discouraged.)
Conclusion
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \rightarrow \exists{!} y \, \exists x \, \varphi \)
Proof
excomim
l1
a1i _
2moswap
l3
anim12d l1 _
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \rightarrow \exists y \, \exists x \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \)
l4
df-eu
\( \vdash \exists{!} x \, \exists y \, \varphi \leftrightarrow \exists x \, \exists y \, \varphi \wedge \exists^\ast x \, \exists y \, \varphi \)
df-eu
\( \vdash \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists y \, \exists x \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \)
3imtr4g l3 l4 _