Theorem 2eu7
Two equivalent expressions for double existential uniqueness. Usage of
this theorem is discouraged because it depends on [ax-13]. (Contributed
by NM, 19-Feb-2005.) (New usage is discouraged.)
Conclusion
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists{!} x \, \exists{!} y \, (\exists x \, \varphi \wedge \exists y \, \varphi) \)
Proof
nfe1
nfeu _
l2
euan _
\( \vdash \exists{!} x \, (\exists{!} y \, \exists x \, \varphi \wedge \exists y \, \varphi) \leftrightarrow \exists{!} y \, \exists x \, \varphi \wedge \exists{!} x \, \exists y \, \varphi \)
ancom
l4
eubii _
\( \vdash \exists{!} y \, (\exists x \, \varphi \wedge \exists y \, \varphi) \leftrightarrow \exists{!} y \, (\exists y \, \varphi \wedge \exists x \, \varphi) \)
nfe1
l6
euan _
\( \vdash \exists{!} y \, (\exists y \, \varphi \wedge \exists x \, \varphi) \leftrightarrow \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \)
ancom
\( \vdash \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists{!} y \, \exists x \, \varphi \wedge \exists y \, \varphi \)
3bitri l4 l6 _
l9
eubii _
\( \vdash \exists{!} x \, \exists{!} y \, (\exists x \, \varphi \wedge \exists y \, \varphi) \leftrightarrow \exists{!} x \, (\exists{!} y \, \exists x \, \varphi \wedge \exists y \, \varphi) \)
ancom
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists{!} y \, \exists x \, \varphi \wedge \exists{!} x \, \exists y \, \varphi \)
3bitr4ri l2 l9 _