Theorem 2mo2

Description: 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 E* x E* y ph . 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)

	Ref	Expression
Assertion	2mo2	$$⊢\left({\exists }^{*}x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\leftrightarrow \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		exdistrv	$$⊢\exists z\exists w\left(\forall x\left(\exists y\phi \to x=z\right)\wedge \forall y\left(\exists x\phi \to y=w\right)\right)\leftrightarrow \left(\exists z\forall x\left(\exists y\phi \to x=z\right)\wedge \exists w\forall y\left(\exists x\phi \to y=w\right)\right)$$
2		jcab	$$⊢\left(\phi \to \left(x=z\wedge y=w\right)\right)\leftrightarrow \left(\left(\phi \to x=z\right)\wedge \left(\phi \to y=w\right)\right)$$
3	2	2albii	$$⊢\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\leftrightarrow \forall x\forall y\left(\left(\phi \to x=z\right)\wedge \left(\phi \to y=w\right)\right)$$
4		19.26-2	$$⊢\forall x\forall y\left(\left(\phi \to x=z\right)\wedge \left(\phi \to y=w\right)\right)\leftrightarrow \left(\forall x\forall y\left(\phi \to x=z\right)\wedge \forall x\forall y\left(\phi \to y=w\right)\right)$$
5		19.23v	$$⊢\forall y\left(\phi \to x=z\right)\leftrightarrow \left(\exists y\phi \to x=z\right)$$
6	5	albii	$$⊢\forall x\forall y\left(\phi \to x=z\right)\leftrightarrow \forall x\left(\exists y\phi \to x=z\right)$$
7		alcom	$$⊢\forall x\forall y\left(\phi \to y=w\right)\leftrightarrow \forall y\forall x\left(\phi \to y=w\right)$$
8		19.23v	$$⊢\forall x\left(\phi \to y=w\right)\leftrightarrow \left(\exists x\phi \to y=w\right)$$
9	8	albii	$$⊢\forall y\forall x\left(\phi \to y=w\right)\leftrightarrow \forall y\left(\exists x\phi \to y=w\right)$$
10	7 9	bitri	$$⊢\forall x\forall y\left(\phi \to y=w\right)\leftrightarrow \forall y\left(\exists x\phi \to y=w\right)$$
11	6 10	anbi12i	$$⊢\left(\forall x\forall y\left(\phi \to x=z\right)\wedge \forall x\forall y\left(\phi \to y=w\right)\right)\leftrightarrow \left(\forall x\left(\exists y\phi \to x=z\right)\wedge \forall y\left(\exists x\phi \to y=w\right)\right)$$
12	3 4 11	3bitri	$$⊢\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\leftrightarrow \left(\forall x\left(\exists y\phi \to x=z\right)\wedge \forall y\left(\exists x\phi \to y=w\right)\right)$$
13	12	2exbii	$$⊢\exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\leftrightarrow \exists z\exists w\left(\forall x\left(\exists y\phi \to x=z\right)\wedge \forall y\left(\exists x\phi \to y=w\right)\right)$$
14		df-mo	$$⊢{\exists }^{*}x\exists y\phi \leftrightarrow \exists z\forall x\left(\exists y\phi \to x=z\right)$$
15		df-mo	$$⊢{\exists }^{*}y\exists x\phi \leftrightarrow \exists w\forall y\left(\exists x\phi \to y=w\right)$$
16	14 15	anbi12i	$$⊢\left({\exists }^{*}x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\leftrightarrow \left(\exists z\forall x\left(\exists y\phi \to x=z\right)\wedge \exists w\forall y\left(\exists x\phi \to y=w\right)\right)$$
17	1 13 16	3bitr4ri	$$⊢\left({\exists }^{*}x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\leftrightarrow \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)$$