Theorem 2eu6 2289

Description: Two equivalent expressions for double existential uniqueness. (Contributed by NM, 2-Feb-2005.) (Revised by Mario Carneiro, 17-Oct-2016.)

Assertion

Ref	Expression
2eu6	⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)))

Distinct variable groups:   x,y,z,w   φ,z,w

Allowed substitution hints:   φ(x, y)

Proof of Theorem 2eu6

Dummy variables v u are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2eu4 2287	. 2 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
2		nfv 1619	. . . . . 6 ⊢ Ⅎzφ
3		nfv 1619	. . . . . 6 ⊢ Ⅎwφ
4		nfs1v 2106	. . . . . 6 ⊢ Ⅎx[z / x][w / y]φ
5		nfs1v 2106	. . . . . . 7 ⊢ Ⅎy[w / y]φ
6	5	nfsb 2109	. . . . . 6 ⊢ Ⅎy[z / x][w / y]φ
7		sbequ12 1919	. . . . . . 7 ⊢ (y = w → (φ ↔ [w / y]φ))
8		sbequ12 1919	. . . . . . 7 ⊢ (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
9	7, 8	sylan9bbr 681	. . . . . 6 ⊢ ((x = z ∧ y = w) → (φ ↔ [z / x][w / y]φ))
10	2, 3, 4, 6, 9	cbvex2 2005	. . . . 5 ⊢ (∃x∃yφ ↔ ∃z∃w[z / x][w / y]φ)
11		equequ2 1686	. . . . . . . . . 10 ⊢ (z = v → (x = z ↔ x = v))
12		equequ2 1686	. . . . . . . . . 10 ⊢ (w = u → (y = w ↔ y = u))
13	11, 12	bi2anan9 843	. . . . . . . . 9 ⊢ ((z = v ∧ w = u) → ((x = z ∧ y = w) ↔ (x = v ∧ y = u)))
14	13	imbi2d 307	. . . . . . . 8 ⊢ ((z = v ∧ w = u) → ((φ → (x = z ∧ y = w)) ↔ (φ → (x = v ∧ y = u))))
15	14	2albidv 1627	. . . . . . 7 ⊢ ((z = v ∧ w = u) → (∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y(φ → (x = v ∧ y = u))))
16	15	cbvex2v 2007	. . . . . 6 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∃v∃u∀x∀y(φ → (x = v ∧ y = u)))
17		nfv 1619	. . . . . . . . 9 ⊢ Ⅎz(φ → (x = v ∧ y = u))
18		nfv 1619	. . . . . . . . 9 ⊢ Ⅎw(φ → (x = v ∧ y = u))
19		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎx(z = v ∧ w = u)
20	4, 19	nfim 1813	. . . . . . . . 9 ⊢ Ⅎx([z / x][w / y]φ → (z = v ∧ w = u))
21		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎy(z = v ∧ w = u)
22	6, 21	nfim 1813	. . . . . . . . 9 ⊢ Ⅎy([z / x][w / y]φ → (z = v ∧ w = u))
23		equequ1 1684	. . . . . . . . . . 11 ⊢ (x = z → (x = v ↔ z = v))
24		equequ1 1684	. . . . . . . . . . 11 ⊢ (y = w → (y = u ↔ w = u))
25	23, 24	bi2anan9 843	. . . . . . . . . 10 ⊢ ((x = z ∧ y = w) → ((x = v ∧ y = u) ↔ (z = v ∧ w = u)))
26	9, 25	imbi12d 311	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → ((φ → (x = v ∧ y = u)) ↔ ([z / x][w / y]φ → (z = v ∧ w = u))))
27	17, 18, 20, 22, 26	cbval2 2004	. . . . . . . 8 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) ↔ ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u)))
28	27	2exbii 1583	. . . . . . 7 ⊢ (∃v∃u∀x∀y(φ → (x = v ∧ y = u)) ↔ ∃v∃u∀z∀w([z / x][w / y]φ → (z = v ∧ w = u)))
29		2mo 2282	. . . . . . 7 ⊢ (∃v∃u∀z∀w([z / x][w / y]φ → (z = v ∧ w = u)) ↔ ∀z∀w∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)))
30	28, 29	bitri 240	. . . . . 6 ⊢ (∃v∃u∀x∀y(φ → (x = v ∧ y = u)) ↔ ∀z∀w∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)))
31	16, 30	bitri 240	. . . . 5 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀z∀w∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)))
32		19.29r2 1598	. . . . 5 ⊢ ((∃z∃w[z / x][w / y]φ ∧ ∀z∀w∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))) → ∃z∃w([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))))
33	10, 31, 32	syl2anb 465	. . . 4 ⊢ ((∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))) → ∃z∃w([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))))
34		2albiim 1612	. . . . . . 7 ⊢ (∀x∀y(φ ↔ (x = z ∧ y = w)) ↔ (∀x∀y(φ → (x = z ∧ y = w)) ∧ ∀x∀y((x = z ∧ y = w) → φ)))
35		ancom 437	. . . . . . 7 ⊢ ((∀x∀y(φ → (x = z ∧ y = w)) ∧ ∀x∀y((x = z ∧ y = w) → φ)) ↔ (∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
36	34, 35	bitri 240	. . . . . 6 ⊢ (∀x∀y(φ ↔ (x = z ∧ y = w)) ↔ (∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
37	36	2exbii 1583	. . . . 5 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) ↔ ∃z∃w(∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
38		nfv 1619	. . . . . . . . . . . 12 ⊢ Ⅎv(([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y))
39		nfv 1619	. . . . . . . . . . . 12 ⊢ Ⅎu(([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y))
40	4	nfsb 2109	. . . . . . . . . . . . . . 15 ⊢ Ⅎx[u / w][z / x][w / y]φ
41	40	nfsb 2109	. . . . . . . . . . . . . 14 ⊢ Ⅎx[v / z][u / w][z / x][w / y]φ
42	4, 41	nfan 1824	. . . . . . . . . . . . 13 ⊢ Ⅎx([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ)
43	42, 19	nfim 1813	. . . . . . . . . . . 12 ⊢ Ⅎx(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))
44	6	nfsb 2109	. . . . . . . . . . . . . . 15 ⊢ Ⅎy[u / w][z / x][w / y]φ
45	44	nfsb 2109	. . . . . . . . . . . . . 14 ⊢ Ⅎy[v / z][u / w][z / x][w / y]φ
46	6, 45	nfan 1824	. . . . . . . . . . . . 13 ⊢ Ⅎy([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ)
47	46, 21	nfim 1813	. . . . . . . . . . . 12 ⊢ Ⅎy(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))
48		sbequ12 1919	. . . . . . . . . . . . . . . 16 ⊢ (y = u → (φ ↔ [u / y]φ))
49		sbequ12 1919	. . . . . . . . . . . . . . . 16 ⊢ (x = v → ([u / y]φ ↔ [v / x][u / y]φ))
50	48, 49	sylan9bbr 681	. . . . . . . . . . . . . . 15 ⊢ ((x = v ∧ y = u) → (φ ↔ [v / x][u / y]φ))
51	3	sbco2 2086	. . . . . . . . . . . . . . . . 17 ⊢ ([u / w][w / y]φ ↔ [u / y]φ)
52	51	sbbii 1653	. . . . . . . . . . . . . . . 16 ⊢ ([v / x][u / w][w / y]φ ↔ [v / x][u / y]φ)
53		nfv 1619	. . . . . . . . . . . . . . . . . 18 ⊢ Ⅎz[u / w][w / y]φ
54	53	sbco2 2086	. . . . . . . . . . . . . . . . 17 ⊢ ([v / z][z / x][u / w][w / y]φ ↔ [v / x][u / w][w / y]φ)
55		sbcom2 2114	. . . . . . . . . . . . . . . . . 18 ⊢ ([z / x][u / w][w / y]φ ↔ [u / w][z / x][w / y]φ)
56	55	sbbii 1653	. . . . . . . . . . . . . . . . 17 ⊢ ([v / z][z / x][u / w][w / y]φ ↔ [v / z][u / w][z / x][w / y]φ)
57	54, 56	bitr3i 242	. . . . . . . . . . . . . . . 16 ⊢ ([v / x][u / w][w / y]φ ↔ [v / z][u / w][z / x][w / y]φ)
58	52, 57	bitr3i 242	. . . . . . . . . . . . . . 15 ⊢ ([v / x][u / y]φ ↔ [v / z][u / w][z / x][w / y]φ)
59	50, 58	syl6bb 252	. . . . . . . . . . . . . 14 ⊢ ((x = v ∧ y = u) → (φ ↔ [v / z][u / w][z / x][w / y]φ))
60	59	anbi2d 684	. . . . . . . . . . . . 13 ⊢ ((x = v ∧ y = u) → (([z / x][w / y]φ ∧ φ) ↔ ([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ)))
61		equequ2 1686	. . . . . . . . . . . . . 14 ⊢ (x = v → (z = x ↔ z = v))
62		equequ2 1686	. . . . . . . . . . . . . 14 ⊢ (y = u → (w = y ↔ w = u))
63	61, 62	bi2anan9 843	. . . . . . . . . . . . 13 ⊢ ((x = v ∧ y = u) → ((z = x ∧ w = y) ↔ (z = v ∧ w = u)))
64	60, 63	imbi12d 311	. . . . . . . . . . . 12 ⊢ ((x = v ∧ y = u) → ((([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y)) ↔ (([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))))
65	38, 39, 43, 47, 64	cbval2 2004	. . . . . . . . . . 11 ⊢ (∀x∀y(([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y)) ↔ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)))
66		equcom 1680	. . . . . . . . . . . . . . 15 ⊢ (z = x ↔ x = z)
67		equcom 1680	. . . . . . . . . . . . . . 15 ⊢ (w = y ↔ y = w)
68	66, 67	anbi12i 678	. . . . . . . . . . . . . 14 ⊢ ((z = x ∧ w = y) ↔ (x = z ∧ y = w))
69	68	imbi2i 303	. . . . . . . . . . . . 13 ⊢ ((([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y)) ↔ (([z / x][w / y]φ ∧ φ) → (x = z ∧ y = w)))
70		impexp 433	. . . . . . . . . . . . 13 ⊢ ((([z / x][w / y]φ ∧ φ) → (x = z ∧ y = w)) ↔ ([z / x][w / y]φ → (φ → (x = z ∧ y = w))))
71	69, 70	bitri 240	. . . . . . . . . . . 12 ⊢ ((([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y)) ↔ ([z / x][w / y]φ → (φ → (x = z ∧ y = w))))
72	71	2albii 1567	. . . . . . . . . . 11 ⊢ (∀x∀y(([z / x][w / y]φ ∧ φ) → (z = x ∧ w = y)) ↔ ∀x∀y([z / x][w / y]φ → (φ → (x = z ∧ y = w))))
73	65, 72	bitr3i 242	. . . . . . . . . 10 ⊢ (∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)) ↔ ∀x∀y([z / x][w / y]φ → (φ → (x = z ∧ y = w))))
74	4, 6	19.21-2 1864	. . . . . . . . . 10 ⊢ (∀x∀y([z / x][w / y]φ → (φ → (x = z ∧ y = w))) ↔ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w))))
75	73, 74	bitri 240	. . . . . . . . 9 ⊢ (∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u)) ↔ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w))))
76	75	anbi2i 675	. . . . . . . 8 ⊢ (([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))) ↔ ([z / x][w / y]φ ∧ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w)))))
77		abai 770	. . . . . . . 8 ⊢ (([z / x][w / y]φ ∧ ∀x∀y(φ → (x = z ∧ y = w))) ↔ ([z / x][w / y]φ ∧ ([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w)))))
78	76, 77	bitr4i 243	. . . . . . 7 ⊢ (([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))) ↔ ([z / x][w / y]φ ∧ ∀x∀y(φ → (x = z ∧ y = w))))
79		2sb6 2113	. . . . . . . 8 ⊢ ([z / x][w / y]φ ↔ ∀x∀y((x = z ∧ y = w) → φ))
80	79	anbi1i 676	. . . . . . 7 ⊢ (([z / x][w / y]φ ∧ ∀x∀y(φ → (x = z ∧ y = w))) ↔ (∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
81	78, 80	bitri 240	. . . . . 6 ⊢ (([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))) ↔ (∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
82	81	2exbii 1583	. . . . 5 ⊢ (∃z∃w([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))) ↔ ∃z∃w(∀x∀y((x = z ∧ y = w) → φ) ∧ ∀x∀y(φ → (x = z ∧ y = w))))
83	37, 82	bitr4i 243	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) ↔ ∃z∃w([z / x][w / y]φ ∧ ∀v∀u(([z / x][w / y]φ ∧ [v / z][u / w][z / x][w / y]φ) → (z = v ∧ w = u))))
84	33, 83	sylibr 203	. . 3 ⊢ ((∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))) → ∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)))
85		bi2 189	. . . . . . 7 ⊢ ((φ ↔ (x = z ∧ y = w)) → ((x = z ∧ y = w) → φ))
86	85	2alimi 1560	. . . . . 6 ⊢ (∀x∀y(φ ↔ (x = z ∧ y = w)) → ∀x∀y((x = z ∧ y = w) → φ))
87	86	2eximi 1577	. . . . 5 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) → ∃z∃w∀x∀y((x = z ∧ y = w) → φ))
88		2exsb 2132	. . . . 5 ⊢ (∃x∃yφ ↔ ∃z∃w∀x∀y((x = z ∧ y = w) → φ))
89	87, 88	sylibr 203	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) → ∃x∃yφ)
90		bi1 178	. . . . . 6 ⊢ ((φ ↔ (x = z ∧ y = w)) → (φ → (x = z ∧ y = w)))
91	90	2alimi 1560	. . . . 5 ⊢ (∀x∀y(φ ↔ (x = z ∧ y = w)) → ∀x∀y(φ → (x = z ∧ y = w)))
92	91	2eximi 1577	. . . 4 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
93	89, 92	jca 518	. . 3 ⊢ (∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)) → (∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
94	84, 93	impbii 180	. 2 ⊢ ((∃x∃yφ ∧ ∃z∃w∀x∀y(φ → (x = z ∧ y = w))) ↔ ∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)))
95	1, 94	bitri 240	1 ⊢ ((∃!x∃yφ ∧ ∃!y∃xφ) ↔ ∃z∃w∀x∀y(φ ↔ (x = z ∧ y = w)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648  ∃!weu 2204

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This proof depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208

This theorem is used by: (None)