Theorem mo2v 2477

Description: Alternate definition of "at most one." Unlike mo2 2479, which is slightly more general, it does not depend on ax-11 2034 and ax-13 2246, whence it is preferable within predicate logic. Elsewhere, most theorems depend on these axioms anyway, so this advantage is no longer important. (Contributed by Wolf Lammen, 27-May-2019.) (Proof shortened by Wolf Lammen, 10-Nov-2019.)

Assertion

Ref	Expression
mo2v	⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem mo2v

Step	Hyp	Ref	Expression
1		df-mo 2475	. 2 ⊢ (∃*𝑥𝜑 ↔ (∃𝑥𝜑 → ∃!𝑥𝜑))
2		df-eu 2474	. . 3 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
3	2	imbi2i 326	. 2 ⊢ ((∃𝑥𝜑 → ∃!𝑥𝜑) ↔ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
4		alnex 1706	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 ↔ ¬ ∃𝑥𝜑)
5		pm2.21 120	. . . . . . . 8 ⊢ (¬ 𝜑 → (𝜑 → 𝑥 = 𝑦))
6	5	alimi 1739	. . . . . . 7 ⊢ (∀𝑥 ¬ 𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
7	4, 6	sylbir 225	. . . . . 6 ⊢ (¬ ∃𝑥𝜑 → ∀𝑥(𝜑 → 𝑥 = 𝑦))
8	7	eximi 1762	. . . . 5 ⊢ (∃𝑦 ¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
9	8	19.23bi 2061	. . . 4 ⊢ (¬ ∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
10		biimp 205	. . . . . 6 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝜑 → 𝑥 = 𝑦))
11	10	alimi 1739	. . . . 5 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝜑 → 𝑥 = 𝑦))
12	11	eximi 1762	. . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
13	9, 12	ja 173	. . 3 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) → ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
14		nfia1 2030	. . . . . 6 ⊢ Ⅎ𝑥(∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
15		id 22	. . . . . . . . . 10 ⊢ (𝜑 → 𝜑)
16		ax12v 2048	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑦 → (𝜑 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
17	16	com12 32	. . . . . . . . . 10 ⊢ (𝜑 → (𝑥 = 𝑦 → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
18	15, 17	embantd 59	. . . . . . . . 9 ⊢ (𝜑 → ((𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
19	18	spsd 2057	. . . . . . . 8 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑)))
20	19	ancld 576	. . . . . . 7 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑))))
21		albiim 1816	. . . . . . 7 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∀𝑥(𝜑 → 𝑥 = 𝑦) ∧ ∀𝑥(𝑥 = 𝑦 → 𝜑)))
22	20, 21	syl6ibr 242	. . . . . 6 ⊢ (𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
23	14, 22	exlimi 2086	. . . . 5 ⊢ (∃𝑥𝜑 → (∀𝑥(𝜑 → 𝑥 = 𝑦) → ∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
24	23	eximdv 1846	. . . 4 ⊢ (∃𝑥𝜑 → (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
25	24	com12 32	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦) → (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
26	13, 25	impbii 199	. 2 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
27	1, 3, 26	3bitri 286	1 ⊢ (∃*𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384  ∀wal 1481  ∃wex 1704  ∃!weu 2470  ∃*wmo 2471

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-10 2019  ax-12 2047

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-ex 1705  df-nf 1710  df-eu 2474  df-mo 2475

This theorem is referenced by:  mo2  2479  eu3v  2498  mo3  2507  sbmo  2515  moim  2519  mopick  2535  2mo2  2550  mo2icl  3385  moabex  4927  dffun3  5899  dffun6f  5902  grothprim  9656  bj-mo3OLD  32832  wl-mo2df  33352  wl-mo2t  33357  wl-mo3t  33358  dffrege115  38272