Theorem 2eu8
Two equivalent expressions for double existential uniqueness. Curiously,
we can put E! on either of the internal conjuncts but not both. We
can also commute E! x E! y using 2eu7. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by NM,
20-Feb-2005.) (New usage is discouraged.)
Conclusion
\( \vdash \exists{!} x \, \exists{!} y \, (\exists x \, \varphi \wedge \exists y \, \varphi) \leftrightarrow \exists{!} x \, \exists{!} y \, (\exists{!} x \, \varphi \wedge \exists y \, \varphi) \)
Proof
2eu2
l1
pm5.32i _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \)
nfeu1
nfeu _
l4
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
l6
eubii _
\( \vdash \exists{!} y \, (\exists{!} x \, \varphi \wedge \exists y \, \varphi) \leftrightarrow \exists{!} y \, (\exists y \, \varphi \wedge \exists{!} x \, \varphi) \)
nfe1
l8
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 l6 l8 _
l11
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 \)
l13
3bitr4ri l4 l11 _
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \exists{!} y \, (\exists{!} x \, \varphi \wedge \exists y \, \varphi) \)
2eu7
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \leftrightarrow \exists{!} x \, \exists{!} y \, (\exists x \, \varphi \wedge \exists y \, \varphi) \)
3bitr3ri l1 l13 _