Theorem 2eu3

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

	Ref	Expression
Assertion	2eu3	$$⊢\forall x\forall y\left({\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\to \left(\left(\exists !x\exists !y\phi \wedge \exists !y\exists !x\phi \right)\leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfmo1	$$⊢Ⅎy{\exists }^{*}y\phi$$
2	1	19.31	$$⊢\forall y\left({\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\leftrightarrow \left(\forall y{\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)$$
3	2	albii	$$⊢\forall x\forall y\left({\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\leftrightarrow \forall x\left(\forall y{\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)$$
4		nfmo1	$$⊢Ⅎx{\exists }^{*}x\phi$$
5	4	nfal	$$⊢Ⅎx\forall y{\exists }^{*}x\phi$$
6	5	19.32	$$⊢\forall x\left(\forall y{\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\leftrightarrow \left(\forall y{\exists }^{*}x\phi \vee \forall x{\exists }^{*}y\phi \right)$$
7	3 6	bitri	$$⊢\forall x\forall y\left({\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\leftrightarrow \left(\forall y{\exists }^{*}x\phi \vee \forall x{\exists }^{*}y\phi \right)$$
8		2eu1	$$⊢\forall y{\exists }^{*}x\phi \to \left(\exists !y\exists !x\phi \leftrightarrow \left(\exists !y\exists x\phi \wedge \exists !x\exists y\phi \right)\right)$$
9	8	biimpd	$$⊢\forall y{\exists }^{*}x\phi \to \left(\exists !y\exists !x\phi \to \left(\exists !y\exists x\phi \wedge \exists !x\exists y\phi \right)\right)$$
10		ancom	$$⊢\left(\exists !y\exists x\phi \wedge \exists !x\exists y\phi \right)\leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)$$
11	9 10	imbitrdi	$$⊢\forall y{\exists }^{*}x\phi \to \left(\exists !y\exists !x\phi \to \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
12		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)$$
13	12	biimpd	$$⊢\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)$$
14	11 13	jaoa	$$⊢\left(\forall y{\exists }^{*}x\phi \vee \forall x{\exists }^{*}y\phi \right)\to \left(\left(\exists !y\exists !x\phi \wedge \exists !x\exists !y\phi \right)\to \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
15	14	ancomsd	$$⊢\left(\forall y{\exists }^{*}x\phi \vee \forall x{\exists }^{*}y\phi \right)\to \left(\left(\exists !x\exists !y\phi \wedge \exists !y\exists !x\phi \right)\to \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
16		2exeu	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !x\exists !y\phi$$
17		2exeu	$$⊢\left(\exists !y\exists x\phi \wedge \exists !x\exists y\phi \right)\to \exists !y\exists !x\phi$$
18	17	ancoms	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \exists !y\exists !x\phi$$
19	16 18	jca	$$⊢\left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\to \left(\exists !x\exists !y\phi \wedge \exists !y\exists !x\phi \right)$$
20	15 19	impbid1	$$⊢\left(\forall y{\exists }^{*}x\phi \vee \forall x{\exists }^{*}y\phi \right)\to \left(\left(\exists !x\exists !y\phi \wedge \exists !y\exists !x\phi \right)\leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$
21	7 20	sylbi	$$⊢\forall x\forall y\left({\exists }^{*}x\phi \vee {\exists }^{*}y\phi \right)\to \left(\left(\exists !x\exists !y\phi \wedge \exists !y\exists !x\phi \right)\leftrightarrow \left(\exists !x\exists y\phi \wedge \exists !y\exists x\phi \right)\right)$$