Theorem 2euswapv
A condition allowing to swap an existential quantifier and a unique
existential quantifier. Version of 2euswap with a disjoint variable
condition, which does not require [ax-13]. (Contributed by NM,
10-Apr-2004.) (Revised by GG, 22-Aug-2023.)
Conclusion
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \rightarrow \exists{!} y \, \exists x \, \varphi \)
Proof
excomim
l1
a1i _
2moswapv
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 _