Theorem 2eu1

Description: Double existential uniqueness. This theorem shows a condition under which a "naive" definition matches the correct one. Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker 2eu1v when possible. (Contributed by NM, 3-Dec-2001) (Proof shortened by Wolf Lammen, 23-Apr-2023) (New usage is discouraged.)

	Ref	Expression
Assertion	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)$$

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		2euswap	$$⊢\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		2exeu	$$⊢\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)$$