Theorem 2eu4

Description: This theorem provides us with a definition of double existential uniqueness ("exactly one x and exactly one y "). Naively one might think (incorrectly) that it could be defined by E! x E! y ph . See 2eu1 for a condition under which the naive definition holds and 2exeu for a one-way implication. See 2eu5 and 2eu8 for alternate definitions. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 14-Sep-2019)

	Ref	Expression
Assertion	2eu4	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		df-eu	$$⊢\exists !x\exists y\phi \leftrightarrow \left(\exists x\exists y\phi \wedge {\exists }^{*}x\exists y\phi \right)$$
2		df-eu	$$⊢\exists !y\exists x\phi \leftrightarrow \left(\exists y\exists x\phi \wedge {\exists }^{*}y\exists x\phi \right)$$
3		excom	$$⊢\exists y\exists x\phi \leftrightarrow \exists x\exists y\phi$$
4	3	anbi1i	$$⊢\left(\exists y\exists x\phi \wedge {\exists }^{*}y\exists x\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)$$
5	2 4	bitri	$$⊢\exists !y\exists x\phi \leftrightarrow \left(\exists x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)$$
6	1 5	anbi12i	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\left(\exists x\exists y\phi \wedge {\exists }^{*}x\exists y\phi \right)\wedge \left(\exists x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\right)$$
7		anandi	$$⊢\left(\exists x\exists y\phi \wedge \left({\exists }^{*}x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\right)\leftrightarrow \left(\left(\exists x\exists y\phi \wedge {\exists }^{*}x\exists y\phi \right)\wedge \left(\exists x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\right)$$
8		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)$$
9	8	anbi2i	$$⊢\left(\exists x\exists y\phi \wedge \left({\exists }^{*}x\exists y\phi \wedge {\exists }^{*}y\exists x\phi \right)\right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$
10	6 7 9	3bitr2i	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\exists x\exists y\phi \wedge \exists z\exists w\forall x\forall y\left(\phi \to \left(x=z\wedge y=w\right)\right)\right)$$