Theorem 2eu3
Double existential uniqueness. Usage of this theorem is discouraged
because it depends on [ax-13]. (Contributed by NM, 3-Dec-2001.) (Proof
shortened by Wolf Lammen, 23-Apr-2023.) (New usage is discouraged.)
Conclusion
\( \vdash \forall x \, \forall y \, (\exists^\ast x \, \varphi \vee \exists^\ast y \, \varphi) \rightarrow (\exists{!} x \, \exists{!} y \, \varphi \wedge \exists{!} y \, \exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi) \)
Proof
nfmo1
19.31 _
l2
albii _
\( \vdash \forall x \, \forall y \, (\exists^\ast x \, \varphi \vee \exists^\ast y \, \varphi) \leftrightarrow \forall x \, (\forall y \, \exists^\ast x \, \varphi \vee \exists^\ast y \, \varphi) \)
nfmo1
nfal _
19.32 _
\( \vdash \forall x \, (\forall y \, \exists^\ast x \, \varphi \vee \exists^\ast y \, \varphi) \leftrightarrow \forall y \, \exists^\ast x \, \varphi \vee \forall x \, \exists^\ast y \, \varphi \)
l6
bitri l2 _
\( \vdash \forall x \, \forall y \, (\exists^\ast x \, \varphi \vee \exists^\ast y \, \varphi) \leftrightarrow \forall y \, \exists^\ast x \, \varphi \vee \forall x \, \exists^\ast y \, \varphi \)
2eu1
l8
biimpd _
\( \vdash \forall y \, \exists^\ast x \, \varphi \rightarrow \exists{!} y \, \exists{!} x \, \varphi \rightarrow \exists{!} y \, \exists x \, \varphi \wedge \exists{!} x \, \exists y \, \varphi \)
ancom
\( \vdash \exists{!} y \, \exists x \, \varphi \wedge \exists{!} x \, \exists y \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi \)
l10
imbitrdi l8 _
2eu1
biimpd _
jaoa l10 _
l14
ancomsd _
l15
2exeu
2exeu
ancoms _
jca l15 _
impbid1 l14 _
\( \vdash \forall y \, \exists^\ast x \, \varphi \vee \forall x \, \exists^\ast y \, \varphi \rightarrow (\exists{!} x \, \exists{!} y \, \varphi \wedge \exists{!} y \, \exists{!} x \, \varphi \leftrightarrow \exists{!} x \, \exists y \, \varphi \wedge \exists{!} y \, \exists x \, \varphi) \)
sylbi l6 _