Theorem 2eu1v
Double existential uniqueness. This theorem shows a condition under
which a "naive" definition matches the correct one. Version of 2eu1
with \( x \) and \( y \) distinct, but not requiring [ax-13]. (Contributed
by NM, 3-Dec-2001.) (Revised by Wolf Lammen, 2-Oct-2023.)
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 \)
2euswapv
\( \vdash \forall x \, \exists^\ast y \, \varphi \rightarrow \exists{!} x \, \exists y \, \varphi \rightarrow \exists{!} y \, \exists x \, \varphi \)
syld l7 _
l10
jcad l7 _
2exeuv
impbid1 l10 _