Theorem 2eu1
Double existential uniqueness. This theorem shows a condition under which
a "naive" definition matches the correct one. Usage of this theorem is
discouraged because it depends on [ax-13]. Use the weaker 2eu1v when
possible. (Contributed by NM, 3-Dec-2001.) (Proof shortened by Wolf
Lammen, 23-Apr-2023.) (New usage is discouraged.)
Conclusion
\( \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) \)
Proof
l0
2eu2ex
\( \vdash \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists x \, \exists y \, \varphi \)
moeu
l2
albii _
\( \vdash \forall x \, \exists^\ast y \, \varphi \leftrightarrow \forall x \, (\exists y \, \varphi \rightarrow \exists{!} y \, \varphi) \)
euim
\( \vdash \exists x \, \exists y \, \varphi \wedge \forall x \, (\exists y \, \varphi \rightarrow \exists{!} y \, \varphi) \rightarrow \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \)
sylan2b l2 _
ex _
\( \vdash \exists x \, \exists y \, \varphi \rightarrow \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \)
syl l0 _
l7
pm2.43b _
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists{!} y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \)
2euswap
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \rightarrow \exists{!} y \, \exists x \, \varphi \)
syld l7 _
l10
jcad l7 _
2exeu
impbid1 l10 _