Theorem mo 2226

Description: Equivalent definitions of "there exists at most one." (Contributed by NM, 7-Aug-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)

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

Allowed substitution hints:   φ(x,y)

Proof of Theorem mo

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mo.1	. . . . . 6 ⊢ Ⅎyφ
2		nfv 1619	. . . . . 6 ⊢ Ⅎy x = z
3	1, 2	nfim 1813	. . . . 5 ⊢ Ⅎy(φ → x = z)
4	3	nfal 1842	. . . 4 ⊢ Ⅎy∀x(φ → x = z)
5		nfv 1619	. . . 4 ⊢ Ⅎz∀x(φ → x = y)
6		equequ2 1686	. . . . . 6 ⊢ (z = y → (x = z ↔ x = y))
7	6	imbi2d 307	. . . . 5 ⊢ (z = y → ((φ → x = z) ↔ (φ → x = y)))
8	7	albidv 1625	. . . 4 ⊢ (z = y → (∀x(φ → x = z) ↔ ∀x(φ → x = y)))
9	4, 5, 8	cbvex 1985	. . 3 ⊢ (∃z∀x(φ → x = z) ↔ ∃y∀x(φ → x = y))
10	1	nfs1 2044	. . . . . . . . 9 ⊢ Ⅎx[y / x]φ
11		nfv 1619	. . . . . . . . 9 ⊢ Ⅎx y = z
12	10, 11	nfim 1813	. . . . . . . 8 ⊢ Ⅎx([y / x]φ → y = z)
13		sbequ2 1650	. . . . . . . . 9 ⊢ (x = y → ([y / x]φ → φ))
14		ax-8 1675	. . . . . . . . 9 ⊢ (x = y → (x = z → y = z))
15	13, 14	imim12d 68	. . . . . . . 8 ⊢ (x = y → ((φ → x = z) → ([y / x]φ → y = z)))
16	3, 12, 15	cbv3 1982	. . . . . . 7 ⊢ (∀x(φ → x = z) → ∀y([y / x]φ → y = z))
17	16	ancli 534	. . . . . 6 ⊢ (∀x(φ → x = z) → (∀x(φ → x = z) ∧ ∀y([y / x]φ → y = z)))
18	3, 12	aaan 1884	. . . . . 6 ⊢ (∀x∀y((φ → x = z) ∧ ([y / x]φ → y = z)) ↔ (∀x(φ → x = z) ∧ ∀y([y / x]φ → y = z)))
19	17, 18	sylibr 203	. . . . 5 ⊢ (∀x(φ → x = z) → ∀x∀y((φ → x = z) ∧ ([y / x]φ → y = z)))
20		prth 554	. . . . . . 7 ⊢ (((φ → x = z) ∧ ([y / x]φ → y = z)) → ((φ ∧ [y / x]φ) → (x = z ∧ y = z)))
21		equtr2 1688	. . . . . . 7 ⊢ ((x = z ∧ y = z) → x = y)
22	20, 21	syl6 29	. . . . . 6 ⊢ (((φ → x = z) ∧ ([y / x]φ → y = z)) → ((φ ∧ [y / x]φ) → x = y))
23	22	2alimi 1560	. . . . 5 ⊢ (∀x∀y((φ → x = z) ∧ ([y / x]φ → y = z)) → ∀x∀y((φ ∧ [y / x]φ) → x = y))
24	19, 23	syl 15	. . . 4 ⊢ (∀x(φ → x = z) → ∀x∀y((φ ∧ [y / x]φ) → x = y))
25	24	exlimiv 1634	. . 3 ⊢ (∃z∀x(φ → x = z) → ∀x∀y((φ ∧ [y / x]φ) → x = y))
26	9, 25	sylbir 204	. 2 ⊢ (∃y∀x(φ → x = y) → ∀x∀y((φ ∧ [y / x]φ) → x = y))
27		nfa2 1855	. . . 4 ⊢ Ⅎy∀x∀y((φ ∧ [y / x]φ) → x = y)
28		sp 1747	. . . . . . . 8 ⊢ (∀y((φ ∧ [y / x]φ) → x = y) → ((φ ∧ [y / x]φ) → x = y))
29	28	exp3a 425	. . . . . . 7 ⊢ (∀y((φ ∧ [y / x]φ) → x = y) → (φ → ([y / x]φ → x = y)))
30	29	com3r 73	. . . . . 6 ⊢ ([y / x]φ → (∀y((φ ∧ [y / x]φ) → x = y) → (φ → x = y)))
31	10, 30	alimd 1764	. . . . 5 ⊢ ([y / x]φ → (∀x∀y((φ ∧ [y / x]φ) → x = y) → ∀x(φ → x = y)))
32	31	com12 27	. . . 4 ⊢ (∀x∀y((φ ∧ [y / x]φ) → x = y) → ([y / x]φ → ∀x(φ → x = y)))
33	27, 32	eximd 1770	. . 3 ⊢ (∀x∀y((φ ∧ [y / x]φ) → x = y) → (∃y[y / x]φ → ∃y∀x(φ → x = y)))
34		alnex 1543	. . . 4 ⊢ (∀y ¬ [y / x]φ ↔ ¬ ∃y[y / x]φ)
35	10	nfn 1793	. . . . . 6 ⊢ Ⅎx ¬ [y / x]φ
36	1	nfn 1793	. . . . . 6 ⊢ Ⅎy ¬ φ
37		sbequ1 1918	. . . . . . . 8 ⊢ (x = y → (φ → [y / x]φ))
38	37	equcoms 1681	. . . . . . 7 ⊢ (y = x → (φ → [y / x]φ))
39	38	con3d 125	. . . . . 6 ⊢ (y = x → (¬ [y / x]φ → ¬ φ))
40	35, 36, 39	cbv3 1982	. . . . 5 ⊢ (∀y ¬ [y / x]φ → ∀x ¬ φ)
41		pm2.21 100	. . . . . 6 ⊢ (¬ φ → (φ → x = y))
42	41	alimi 1559	. . . . 5 ⊢ (∀x ¬ φ → ∀x(φ → x = y))
43		19.8a 1756	. . . . 5 ⊢ (∀x(φ → x = y) → ∃y∀x(φ → x = y))
44	40, 42, 43	3syl 18	. . . 4 ⊢ (∀y ¬ [y / x]φ → ∃y∀x(φ → x = y))
45	34, 44	sylbir 204	. . 3 ⊢ (¬ ∃y[y / x]φ → ∃y∀x(φ → x = y))
46	33, 45	pm2.61d1 151	. 2 ⊢ (∀x∀y((φ ∧ [y / x]φ) → x = y) → ∃y∀x(φ → x = y))
47	26, 46	impbii 180	1 ⊢ (∃y∀x(φ → x = y) ↔ ∀x∀y((φ ∧ [y / x]φ) → x = y))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540  ∃wex 1541  Ⅎwnf 1544   = 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:  eu2  2229  eu3  2230  mo3  2235