Theorem eu6 2585

Description: Alternate definition of the unique existential quantifier df-eu 2580 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 2580 was then proved as dfeu 2607. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.)

Assertion

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

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsb 2290	. . 3 ⊢ (∃𝑥𝜑 ↔ ∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑))
2	1	anbi1i 614	. 2 ⊢ ((∃𝑥𝜑 ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
3		eu3v 2581	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
4		eu6lem 2584	. 2 ⊢ (∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦) ↔ (∃𝑦∀𝑥(𝑥 = 𝑦 → 𝜑) ∧ ∃𝑧∀𝑥(𝜑 → 𝑥 = 𝑧)))
5	2, 3, 4	3bitr4i 295	1 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))

Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387  ∀wal 1505  ∃wex 1742  ∃!weu 2579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-10 2077  ax-11 2091  ax-12 2104

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-nf 1747  df-mo 2544  df-eu 2580

This theorem is referenced by:  euf  2588  eufOLD  2589  nfeu1  2602  dfmo  2608  euequOLD  2610  eubidvOLD  2613  nfeud2OLD  2616  eubidOLDOLD  2620  euexOLD  2622  sb8eulem  2626  euaeOLD  2687  reu6  3625  euabsn2  4529  eunex  5137  euotd  5252  iotauni  6158  iota1  6160  iotanul  6161  iotaex  6163  iota4  6164  fv3  6511  eufnfv  6811  seqomlem2  7883  aceq1  9329  dfac5  9340  bnj89  31600  bj-eunex  33567  cbveud  34030  wl-eudf  34197  wl-euequf  34199  wl-sb8eut  34202  iotain  40110  iotaexeu  40111  iotasbc  40112  iotavalsb  40126  sbiota1  40127  eusnsn  42612