Theorem 2eu2
Double existential uniqueness. Usage of this theorem is discouraged
because it depends on [ax-13]. (Contributed by NM, 3-Dec-2001.)
(New usage is discouraged.)
Conclusion
\( \vdash \exists{!} y \, \exists x \, \varphi \rightarrow (\exists{!} x \, \exists{!} y \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi) \)
Proof
l0
eumo
\( \vdash \exists{!} y \, \exists x \, \varphi \rightarrow \exists^\ast y \, \exists x \, \varphi \)
l1
2moex
\( \vdash \exists^\ast y \, \exists x \, \varphi \rightarrow \forall x \, \exists^\ast y \, \varphi \)
l2
2eu1
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow (\exists{!} x \, \exists{!} y \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi) \)
simpl
\( \vdash \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \)
biimtrdi l2 _
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \)
l5
3syl l0 l1 _
2exeu
expcom _
impbid l5 _