Theorem mo 1391

Description: Equivalent definitions of "there exists at most one."

Hypothesis

Ref	Expression
mo.1	⊢ (φ → ∀yφ)

Assertion

Ref	Expression
mo	⊢ (∃y∀x(φ → x = y) ↔ ∀x∀y((φ ⋀ [y / x]φ) → x = y))

Distinct variable group:   x,y

Proof of Theorem mo

Step	Hyp	Ref	Expression
1		mo.1	. . . . . 6 ⊢ (φ → ∀yφ)
2		ax-17 969	. . . . . 6 ⊢ (x = z → ∀y x = z)
3	1, 2	hbim 1005	. . . . 5 ⊢ ((φ → x = z) → ∀y(φ → x = z))
4	3	hbal 1003	. . . 4 ⊢ (∀x(φ → x = z) → ∀y∀x(φ → x = z))
5		ax-17 969	. . . 4 ⊢ (∀x(φ → x = y) → ∀z∀x(φ → x = y))
6		equequ2 1133	. . . . . 6 ⊢ (z = y → (x = z ↔ x = y))
7	6	imbi2d 611	. . . . 5 ⊢ (z = y → ((φ → x = z) ↔ (φ → x = y)))
8	7	albidv 1276	. . . 4 ⊢ (z = y → (∀x(φ → x = z) ↔ ∀x(φ → x = y)))
9	4, 5, 8	cbvex 1164	. . 3 ⊢ (∃z∀x(φ → x = z) ↔ ∃y∀x(φ → x = y))
10		hbs1 1330	. . . . . . . . 9 ⊢ ([y / x]φ → ∀x[y / x]φ)
11		ax-17 969	. . . . . . . . 9 ⊢ (y = z → ∀x y = z)
12	10, 11	hbim 1005	. . . . . . . 8 ⊢ (([y / x]φ → y = z) → ∀x([y / x]φ → y = z))
13		sbequ2 1177	. . . . . . . . 9 ⊢ (x = y → ([y / x]φ → φ))
14		ax-8 962	. . . . . . . . 9 ⊢ (x = y → (x = z → y = z))
15	13, 14	imim12d 29	. . . . . . . 8 ⊢ (x = y → ((φ → x = z) → ([y / x]φ → y = z)))
16	3, 12, 15	cbv3 1162	. . . . . . 7 ⊢ (∀x(φ → x = z) → ∀y([y / x]φ → y = z))
17	16	ancli 296	. . . . . 6 ⊢ (∀x(φ → x = z) → (∀x(φ → x = z) ⋀ ∀y([y / x]φ → y = z)))
18	3, 12	aaan 1117	. . . . . 6 ⊢ (∀x∀y((φ → x = z) ⋀ ([y / x]φ → y = z)) ↔ (∀x(φ → x = z) ⋀ ∀y([y / x]φ → y = z)))
19	17, 18	sylibr 200	. . . . 5 ⊢ (∀x(φ → x = z) → ∀x∀y((φ → x = z) ⋀ ([y / x]φ → y = z)))
20		prth 555	. . . . . . 7 ⊢ (((φ → x = z) ⋀ ([y / x]φ → y = z)) → ((φ ⋀ [y / x]φ) → (x = z ⋀ y = z)))
21		equtr2 1131	. . . . . . 7 ⊢ ((x = z ⋀ y = z) → x = y)
22	20, 21	syl6 22	. . . . . 6 ⊢ (((φ → x = z) ⋀ ([y / x]φ → y = z)) → ((φ ⋀ [y / x]φ) → x = y))
23	22	19.20i2 991	. . . . 5 ⊢ (∀x∀y((φ → x = z) ⋀ ([y / x]φ → y = z)) → ∀x∀y((φ ⋀ [y / x]φ) → x = y))
24	19, 23	syl 10	. . . 4 ⊢ (∀x(φ → x = z) → ∀x∀y((φ ⋀ [y / x]φ) → x = y))
25	24	19.23aiv 1293	. . 3 ⊢ (∃z∀x(φ → x = z) → ∀x∀y((φ ⋀ [y / x]φ) → x = y))
26	9, 25	sylbir 201	. 2 ⊢ (∃y∀x(φ → x = y) → ∀x∀y((φ ⋀ [y / x]φ) → x = y))
27		19.20 992	. . . . . . . 8 ⊢ (∀x([y / x]φ → (φ → x = y)) → (∀x[y / x]φ → ∀x(φ → x = y)))
28	27	19.20i 990	. . . . . . 7 ⊢ (∀y∀x([y / x]φ → (φ → x = y)) → ∀y(∀x[y / x]φ → ∀x(φ → x = y)))
29	28	a7s 989	. . . . . 6 ⊢ (∀x∀y([y / x]φ → (φ → x = y)) → ∀y(∀x[y / x]φ → ∀x(φ → x = y)))
30		19.22 1037	. . . . . 6 ⊢ (∀y(∀x[y / x]φ → ∀x(φ → x = y)) → (∃y∀x[y / x]φ → ∃y∀x(φ → x = y)))
31	29, 30	syl 10	. . . . 5 ⊢ (∀x∀y([y / x]φ → (φ → x = y)) → (∃y∀x[y / x]φ → ∃y∀x(φ → x = y)))
32	1	hbsb3 1204	. . . . . 6 ⊢ ([y / x]φ → ∀x[y / x]φ)
33	32	19.22i 1038	. . . . 5 ⊢ (∃y[y / x]φ → ∃y∀x[y / x]φ)
34	31, 33	syl5com 52	. . . 4 ⊢ (∃y[y / x]φ → (∀x∀y([y / x]φ → (φ → x = y)) → ∃y∀x(φ → x = y)))
35		impexp 347	. . . . . 6 ⊢ (((φ ⋀ [y / x]φ) → x = y) ↔ (φ → ([y / x]φ → x = y)))
36		bi2.04 160	. . . . . 6 ⊢ ((φ → ([y / x]φ → x = y)) ↔ ([y / x]φ → (φ → x = y)))
37	35, 36	bitr 173	. . . . 5 ⊢ (((φ ⋀ [y / x]φ) → x = y) ↔ ([y / x]φ → (φ → x = y)))
38	37	2albii 998	. . . 4 ⊢ (∀x∀y((φ ⋀ [y / x]φ) → x = y) ↔ ∀x∀y([y / x]φ → (φ → x = y)))
39	34, 38	syl5ib 206	. . 3 ⊢ (∃y[y / x]φ → (∀x∀y((φ ⋀ [y / x]φ) → x = y) → ∃y∀x(φ → x = y)))
40		alnex 1031	. . . . 5 ⊢ (∀y ¬ [y / x]φ ↔ ¬ ∃y[y / x]φ)
41	32	hbn 1002	. . . . . . 7 ⊢ (¬ [y / x]φ → ∀x ¬ [y / x]φ)
42	1	hbn 1002	. . . . . . 7 ⊢ (¬ φ → ∀y ¬ φ)
43		sbequ1 1176	. . . . . . . . 9 ⊢ (x = y → (φ → [y / x]φ))
44	43	equcoms 1128	. . . . . . . 8 ⊢ (y = x → (φ → [y / x]φ))
45	44	con3d 95	. . . . . . 7 ⊢ (y = x → (¬ [y / x]φ → ¬ φ))
46	41, 42, 45	cbv3 1162	. . . . . 6 ⊢ (∀y ¬ [y / x]φ → ∀x ¬ φ)
47		pm2.21 76	. . . . . . 7 ⊢ (¬ φ → (φ → x = y))
48	47	19.20i 990	. . . . . 6 ⊢ (∀x ¬ φ → ∀x(φ → x = y))
49		19.8a 1027	. . . . . 6 ⊢ (∀x(φ → x = y) → ∃y∀x(φ → x = y))
50	46, 48, 49	3syl 20	. . . . 5 ⊢ (∀y ¬ [y / x]φ → ∃y∀x(φ → x = y))
51	40, 50	sylbir 201	. . . 4 ⊢ (¬ ∃y[y / x]φ → ∃y∀x(φ → x = y))
52	51	a1d 12	. . 3 ⊢ (¬ ∃y[y / x]φ → (∀x∀y((φ ⋀ [y / x]φ) → x = y) → ∃y∀x(φ → x = y)))
53	39, 52	pm2.61i 126	. 2 ⊢ (∀x∀y((φ ⋀ [y / x]φ) → x = y) → ∃y∀x(φ → x = y))
54	26, 53	impbi 157	1 ⊢ (∃y∀x(φ → x = y) ↔ ∀x∀y((φ ⋀ [y / x]φ) → x = y))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954  ∃wex 978  [wsbc 1168

This theorem is referenced by:  eu2 1394  eu3 1395  mo3 1399

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-11 965  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain