Theorem 2eu5OLD

Description: Obsolete version of 2eu5 as of 2-Oct-2023. (Contributed by NM, 26-Oct-2003) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	2eu5OLD	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\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		2eu1	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
2	1	pm5.32ri	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\phi \right)\leftrightarrow \left(\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\wedge \forall x{\exists }^{*}y\phi \right)$$
3		eumo	$$⊢\exists !y\exists x\phi \to {\exists }^{*}y\exists x\phi$$
4	3	adantl	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to {\exists }^{*}y\exists x\phi$$
5		2moex	$$⊢{\exists }^{*}y\exists x\phi \to \forall x{\exists }^{*}y\phi$$
6	4 5	syl	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \forall x{\exists }^{*}y\phi$$
7	6	pm4.71i	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\leftrightarrow \left(\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\wedge \forall x{\exists }^{*}y\phi \right)$$
8		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)$$
9	2 7 8	3bitr2i	$$⊢\left(\exists !x\exists !y\phi \wedge \forall x{\exists }^{*}y\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)$$