Theorem 2eu1v

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. Version of 2eu1 with x and y distinct, but not requiring ax-13 . (Contributed by NM, 3-Dec-2001) (Revised by Wolf Lammen, 2-Oct-2023)

	Ref	Expression
Assertion	2eu1v	$$⊢\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)$$

Proof

Step	Hyp	Ref	Expression
1		2eu2ex	$$⊢\exists !x\exists !y\phi \to \exists x\exists y\phi$$
2		moeu	$$⊢{\exists }^{*}y\phi \leftrightarrow \left(\exists y\phi \to \exists !y\phi \right)$$
3	2	albii	$$⊢\forall x{\exists }^{*}y\phi \leftrightarrow \forall x\left(\exists y\phi \to \exists !y\phi \right)$$
4		euim	$$⊢\left(\exists x\exists y\phi \wedge \forall x\left(\exists y\phi \to \exists !y\phi \right)\right)\to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)$$
5	3 4	sylan2b	$$⊢\left(\exists x\exists y\phi \wedge \forall x{\exists }^{*}y\phi \right)\to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)$$
6	5	ex	$$⊢\exists x\exists y\phi \to \left(\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)\right)$$
7	1 6	syl	$$⊢\exists !x\exists !y\phi \to \left(\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)\right)$$
8	7	pm2.43b	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \exists !x\exists y\phi \right)$$
9		2euswapv	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists y\phi \to \exists !y\exists x\phi \right)$$
10	8 9	syld	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \exists !y\exists x\phi \right)$$
11	8 10	jcad	$$⊢\forall x{\exists }^{*}y\phi \to \left(\exists !x\exists !y\phi \to \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
12		2exeuv	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists !y\phi$$
13	11 12	impbid1	$$⊢\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)$$