Theorem eu6 2608

Description: Alternate definition of the unique existential quantifier df-eu 2603 not using the at-most-one quantifier. (Contributed by NM, 12-Aug-1993.) This used to be the definition of the unique existential quantifier, while df-eu 2603 was then proved as dfeu 2629. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2198. (Revised by SN, 21-Sep-2023.)

Assertion

Ref	Expression
eu6	⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6

Step	Hyp	Ref	Expression
1		dfmoeu 2569	. . . 4 ⊢ ((∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦))
2	1	anbi2i 634	. . 3 ⊢ ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
3		abai 838	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))))
4		eu3v 2604	. . 3 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 → 𝑥 = 𝑦)))
5	2, 3, 4	3bitr4ri 307	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)))
6		abai 838	. . 3 ⊢ ((∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
7		ancom 465	. . 3 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8		biimpr 223	. . . . . . 7 ⊢ ((𝜑 ↔ 𝑥 = 𝑦) → (𝑥 = 𝑦 → 𝜑))
9	8	alimi 1838	. . . . . 6 ⊢ (∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦 → 𝜑))
10	9	eximi 1862	. . . . 5 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
11		exsbim 2029	. . . . 5 ⊢ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) → ∃𝑥𝜑)
12	10, 11	syl 18	. . . 4 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)
13	12	biantru 538	. . 3 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ∧ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) → ∃𝑥𝜑)))
14	6, 7, 13	3bitr4i 306	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)) ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
15	5, 14	bitri 278	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1565  ∃wex 1806  ∃!weu 2602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-12 2219

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1807  df-nf 1811  df-mo 2573  df-eu 2603

This theorem is referenced by:  euf  2610  nfeu1ALT  2622  dfmo2  2630  sb8eulem  2632  reu6  3698  euabsn2  4696  eunex  5362  euotd  5497  iotauni  6514  iota1  6516  iotanul  6517  iota4  6518  fv3  6900  eufnfv  7228  seqomlem2  8438  aceq1  10101  dfac5  10112  bnj89  35055  cbveud  37940  wl-eudf  38149  wl-euequf  38151  wl-sb8eut  38155  wl-sb8eutv  38156  iotain  45053  iotaexeu  45054  iotasbc  45055  iotavalsb  45069  sbiota1  45070  dfac5prim  45625  permac8prim  45649  eusnsn  47686  mo0sn  49513