Theorem 2mo2
Two ways of expressing "there exists at most one ordered pair
<. x , y >. such that ph ( x , y ) holds. Note that this is not
equivalent to \( \exists^\ast x \, \exists^\ast y \, \varphi \). See also 2mo. This is the analogue
of 2eu4 for existential uniqueness. (Contributed by Wolf Lammen,
26-Oct-2019.) Reduce dependencies on axioms. (Revised by Wolf Lammen,
3-Jan-2023.)
Conclusion
\( \vdash \exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \leftrightarrow \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \)
Proof
l0
exdistrv
\( \vdash \exists z \, \exists w \, (\forall x \, (\exists y \, \varphi \rightarrow x = z) \wedge \forall y \, (\exists x \, \varphi \rightarrow y = w)) \leftrightarrow \exists z \, \forall x \, (\exists y \, \varphi \rightarrow x = z) \wedge \exists w \, \forall y \, (\exists x \, \varphi \rightarrow y = w) \)
jcab
l2
2albii _
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \forall x \, \forall y \, ((\varphi \rightarrow x = z) \wedge (\varphi \rightarrow y = w)) \)
l3
19.26-2
\( \vdash \forall x \, \forall y \, ((\varphi \rightarrow x = z) \wedge (\varphi \rightarrow y = w)) \leftrightarrow \forall x \, \forall y \, (\varphi \rightarrow x = z) \wedge \forall x \, \forall y \, (\varphi \rightarrow y = w) \)
19.23v
l5
albii _
l6
alcom
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow y = w) \leftrightarrow \forall y \, \forall x \, (\varphi \rightarrow y = w) \)
19.23v
albii _
\( \vdash \forall y \, \forall x \, (\varphi \rightarrow y = w) \leftrightarrow \forall y \, (\exists x \, \varphi \rightarrow y = w) \)
bitri l6 _
anbi12i l5 _
\( \vdash \forall x \, \forall y \, (\varphi \rightarrow x = z) \wedge \forall x \, \forall y \, (\varphi \rightarrow y = w) \leftrightarrow \forall x \, (\exists y \, \varphi \rightarrow x = z) \wedge \forall y \, (\exists x \, \varphi \rightarrow y = w) \)
3bitri l2 l3 _
l12
2exbii _
\( \vdash \exists z \, \exists w \, \forall x \, \forall y \, (\varphi \rightarrow x = z \wedge y = w) \leftrightarrow \exists z \, \exists w \, (\forall x \, (\exists y \, \varphi \rightarrow x = z) \wedge \forall y \, (\exists x \, \varphi \rightarrow y = w)) \)
l13
dfmo
dfmo
anbi12i l13 _
\( \vdash \exists^\ast x \, \exists y \, \varphi \wedge \exists^\ast y \, \exists x \, \varphi \leftrightarrow \exists z \, \forall x \, (\exists y \, \varphi \rightarrow x = z) \wedge \exists w \, \forall y \, (\exists x \, \varphi \rightarrow y = w) \)
3bitr4ri l0 l12 _