Theorem 2eu2

Description: Double existential uniqueness. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 3-Dec-2001) (New usage is discouraged.)

	Ref	Expression
Assertion	2eu2	$$⊢\exists !y\exists x\phi \to \left(\exists !x\exists !y\phi \leftrightarrow \exists !x\exists y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		eumo	$$⊢\exists !y\exists x\phi \to {\exists }^{*}y\exists x\phi$$
2		2moex	$$⊢{\exists }^{*}y\exists x\phi \to \forall x{\exists }^{*}y\phi$$
3		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)$$
4		simpl	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists y\phi$$
5	3 4	biimtrdi	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)$$
6	1 2 5	3syl	$$⊢\exists !y\exists x\phi \to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)$$
7		2exeu	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists !y\phi$$
8	7	expcom	$$⊢\exists !y\exists x\phi \to \left(\exists !x\exists y\phi \to \exists !x\exists !y\phi \right)$$
9	6 8	impbid	$$⊢\exists !y\exists x\phi \to \left(\exists !x\exists !y\phi \leftrightarrow \exists !x\exists y\phi \right)$$