Theorem 2mo 2282

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

Assertion

Ref	Expression
2mo	⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))

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

Allowed substitution hints:   φ(x,y)

Proof of Theorem 2mo

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

Step	Hyp	Ref	Expression
1		equequ2 1686	. . . . . . 7 ⊢ (v = z → (x = v ↔ x = z))
2		equequ2 1686	. . . . . . 7 ⊢ (u = w → (y = u ↔ y = w))
3	1, 2	bi2anan9 843	. . . . . 6 ⊢ ((v = z ∧ u = w) → ((x = v ∧ y = u) ↔ (x = z ∧ y = w)))
4	3	imbi2d 307	. . . . 5 ⊢ ((v = z ∧ u = w) → ((φ → (x = v ∧ y = u)) ↔ (φ → (x = z ∧ y = w))))
5	4	2albidv 1627	. . . 4 ⊢ ((v = z ∧ u = w) → (∀x∀y(φ → (x = v ∧ y = u)) ↔ ∀x∀y(φ → (x = z ∧ y = w))))
6	5	cbvex2v 2007	. . 3 ⊢ (∃v∃u∀x∀y(φ → (x = v ∧ y = u)) ↔ ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
7		nfv 1619	. . . . . . . . 9 ⊢ Ⅎz(φ → (x = v ∧ y = u))
8		nfv 1619	. . . . . . . . 9 ⊢ Ⅎw(φ → (x = v ∧ y = u))
9		nfs1v 2106	. . . . . . . . . 10 ⊢ Ⅎx[z / x][w / y]φ
10		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎx(z = v ∧ w = u)
11	9, 10	nfim 1813	. . . . . . . . 9 ⊢ Ⅎx([z / x][w / y]φ → (z = v ∧ w = u))
12		nfs1v 2106	. . . . . . . . . . 11 ⊢ Ⅎy[w / y]φ
13	12	nfsb 2109	. . . . . . . . . 10 ⊢ Ⅎy[z / x][w / y]φ
14		nfv 1619	. . . . . . . . . 10 ⊢ Ⅎy(z = v ∧ w = u)
15	13, 14	nfim 1813	. . . . . . . . 9 ⊢ Ⅎy([z / x][w / y]φ → (z = v ∧ w = u))
16		sbequ12 1919	. . . . . . . . . . 11 ⊢ (y = w → (φ ↔ [w / y]φ))
17		sbequ12 1919	. . . . . . . . . . 11 ⊢ (x = z → ([w / y]φ ↔ [z / x][w / y]φ))
18	16, 17	sylan9bbr 681	. . . . . . . . . 10 ⊢ ((x = z ∧ y = w) → (φ ↔ [z / x][w / y]φ))
19		equequ1 1684	. . . . . . . . . . 11 ⊢ (x = z → (x = v ↔ z = v))
20		equequ1 1684	. . . . . . . . . . 11 ⊢ (y = w → (y = u ↔ w = u))
21	19, 20	bi2anan9 843	. . . . . . . . . 10 ⊢ ((x = z ∧ y = w) → ((x = v ∧ y = u) ↔ (z = v ∧ w = u)))
22	18, 21	imbi12d 311	. . . . . . . . 9 ⊢ ((x = z ∧ y = w) → ((φ → (x = v ∧ y = u)) ↔ ([z / x][w / y]φ → (z = v ∧ w = u))))
23	7, 8, 11, 15, 22	cbval2 2004	. . . . . . . 8 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) ↔ ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u)))
24	23	biimpi 186	. . . . . . 7 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) → ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u)))
25	24	ancli 534	. . . . . 6 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) → (∀x∀y(φ → (x = v ∧ y = u)) ∧ ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u))))
26		alcom 1737	. . . . . . . . 9 ⊢ (∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ ∀z∀y∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))))
27	8, 15	aaan 1884	. . . . . . . . . 10 ⊢ (∀y∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ (∀y(φ → (x = v ∧ y = u)) ∧ ∀w([z / x][w / y]φ → (z = v ∧ w = u))))
28	27	albii 1566	. . . . . . . . 9 ⊢ (∀z∀y∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ ∀z(∀y(φ → (x = v ∧ y = u)) ∧ ∀w([z / x][w / y]φ → (z = v ∧ w = u))))
29	26, 28	bitri 240	. . . . . . . 8 ⊢ (∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ ∀z(∀y(φ → (x = v ∧ y = u)) ∧ ∀w([z / x][w / y]φ → (z = v ∧ w = u))))
30	29	albii 1566	. . . . . . 7 ⊢ (∀x∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ ∀x∀z(∀y(φ → (x = v ∧ y = u)) ∧ ∀w([z / x][w / y]φ → (z = v ∧ w = u))))
31		nfv 1619	. . . . . . . 8 ⊢ Ⅎz∀y(φ → (x = v ∧ y = u))
32	11	nfal 1842	. . . . . . . 8 ⊢ Ⅎx∀w([z / x][w / y]φ → (z = v ∧ w = u))
33	31, 32	aaan 1884	. . . . . . 7 ⊢ (∀x∀z(∀y(φ → (x = v ∧ y = u)) ∧ ∀w([z / x][w / y]φ → (z = v ∧ w = u))) ↔ (∀x∀y(φ → (x = v ∧ y = u)) ∧ ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u))))
34	30, 33	bitri 240	. . . . . 6 ⊢ (∀x∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) ↔ (∀x∀y(φ → (x = v ∧ y = u)) ∧ ∀z∀w([z / x][w / y]φ → (z = v ∧ w = u))))
35	25, 34	sylibr 203	. . . . 5 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) → ∀x∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))))
36		prth 554	. . . . . . . 8 ⊢ (((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) → ((φ ∧ [z / x][w / y]φ) → ((x = v ∧ y = u) ∧ (z = v ∧ w = u))))
37		equtr2 1688	. . . . . . . . . 10 ⊢ ((x = v ∧ z = v) → x = z)
38		equtr2 1688	. . . . . . . . . 10 ⊢ ((y = u ∧ w = u) → y = w)
39	37, 38	anim12i 549	. . . . . . . . 9 ⊢ (((x = v ∧ z = v) ∧ (y = u ∧ w = u)) → (x = z ∧ y = w))
40	39	an4s 799	. . . . . . . 8 ⊢ (((x = v ∧ y = u) ∧ (z = v ∧ w = u)) → (x = z ∧ y = w))
41	36, 40	syl6 29	. . . . . . 7 ⊢ (((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) → ((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
42	41	2alimi 1560	. . . . . 6 ⊢ (∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) → ∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
43	42	2alimi 1560	. . . . 5 ⊢ (∀x∀y∀z∀w((φ → (x = v ∧ y = u)) ∧ ([z / x][w / y]φ → (z = v ∧ w = u))) → ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
44	35, 43	syl 15	. . . 4 ⊢ (∀x∀y(φ → (x = v ∧ y = u)) → ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
45	44	exlimivv 1635	. . 3 ⊢ (∃v∃u∀x∀y(φ → (x = v ∧ y = u)) → ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
46	6, 45	sylbir 204	. 2 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) → ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
47		alrot4 1739	. . . . 5 ⊢ (∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) ↔ ∀z∀w∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))
48		pm3.21 435	. . . . . . . . . . . 12 ⊢ ([z / x][w / y]φ → (φ → (φ ∧ [z / x][w / y]φ)))
49	48	imim1d 69	. . . . . . . . . . 11 ⊢ ([z / x][w / y]φ → (((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → (φ → (x = z ∧ y = w))))
50	13, 49	alimd 1764	. . . . . . . . . 10 ⊢ ([z / x][w / y]φ → (∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∀y(φ → (x = z ∧ y = w))))
51	9, 50	alimd 1764	. . . . . . . . 9 ⊢ ([z / x][w / y]φ → (∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∀x∀y(φ → (x = z ∧ y = w))))
52	51	com12 27	. . . . . . . 8 ⊢ (∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w))))
53	52	alimi 1559	. . . . . . 7 ⊢ (∀w∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∀w([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w))))
54		exim 1575	. . . . . . 7 ⊢ (∀w([z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w))) → (∃w[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ∧ y = w))))
55	53, 54	syl 15	. . . . . 6 ⊢ (∀w∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → (∃w[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ∧ y = w))))
56	55	alimi 1559	. . . . 5 ⊢ (∀z∀w∀x∀y((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∀z(∃w[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ∧ y = w))))
57	47, 56	sylbi 187	. . . 4 ⊢ (∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∀z(∃w[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ∧ y = w))))
58		exim 1575	. . . 4 ⊢ (∀z(∃w[z / x][w / y]φ → ∃w∀x∀y(φ → (x = z ∧ y = w))) → (∃z∃w[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
59	57, 58	syl 15	. . 3 ⊢ (∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → (∃z∃w[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ∧ y = w))))
60		alnex 1543	. . . . . 6 ⊢ (∀w ¬ [z / x][w / y]φ ↔ ¬ ∃w[z / x][w / y]φ)
61	60	albii 1566	. . . . 5 ⊢ (∀z∀w ¬ [z / x][w / y]φ ↔ ∀z ¬ ∃w[z / x][w / y]φ)
62		alnex 1543	. . . . 5 ⊢ (∀z ¬ ∃w[z / x][w / y]φ ↔ ¬ ∃z∃w[z / x][w / y]φ)
63	61, 62	bitri 240	. . . 4 ⊢ (∀z∀w ¬ [z / x][w / y]φ ↔ ¬ ∃z∃w[z / x][w / y]φ)
64		nfv 1619	. . . . . . 7 ⊢ Ⅎz ¬ φ
65		nfv 1619	. . . . . . 7 ⊢ Ⅎw ¬ φ
66	9	nfn 1793	. . . . . . 7 ⊢ Ⅎx ¬ [z / x][w / y]φ
67	13	nfn 1793	. . . . . . 7 ⊢ Ⅎy ¬ [z / x][w / y]φ
68	18	notbid 285	. . . . . . 7 ⊢ ((x = z ∧ y = w) → (¬ φ ↔ ¬ [z / x][w / y]φ))
69	64, 65, 66, 67, 68	cbval2 2004	. . . . . 6 ⊢ (∀x∀y ¬ φ ↔ ∀z∀w ¬ [z / x][w / y]φ)
70		pm2.21 100	. . . . . . 7 ⊢ (¬ φ → (φ → (x = z ∧ y = w)))
71	70	2alimi 1560	. . . . . 6 ⊢ (∀x∀y ¬ φ → ∀x∀y(φ → (x = z ∧ y = w)))
72	69, 71	sylbir 204	. . . . 5 ⊢ (∀z∀w ¬ [z / x][w / y]φ → ∀x∀y(φ → (x = z ∧ y = w)))
73		19.8a 1756	. . . . . 6 ⊢ (∃w∀x∀y(φ → (x = z ∧ y = w)) → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
74	73	19.23bi 1759	. . . . 5 ⊢ (∀x∀y(φ → (x = z ∧ y = w)) → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
75	72, 74	syl 15	. . . 4 ⊢ (∀z∀w ¬ [z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
76	63, 75	sylbir 204	. . 3 ⊢ (¬ ∃z∃w[z / x][w / y]φ → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
77	59, 76	pm2.61d1 151	. 2 ⊢ (∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)) → ∃z∃w∀x∀y(φ → (x = z ∧ y = w)))
78	46, 77	impbii 180	1 ⊢ (∃z∃w∀x∀y(φ → (x = z ∧ y = w)) ↔ ∀x∀y∀z∀w((φ ∧ [z / x][w / y]φ) → (x = z ∧ y = w)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541   = wceq 1642  [wsb 1648

This theorem was proved from 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 theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649

This theorem is referenced by:  2mos  2283  2eu6  2289