MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eu6 Structured version   Visualization version   GIF version

Theorem eu6 2568
Description: Alternate definition of the unique existential quantifier df-eu 2563 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 2563 was then proved as dfeu 2589. (Revised by BJ, 30-Sep-2022.) (Proof shortened by Wolf Lammen, 3-Jan-2023.) Remove use of ax-11 2154. (Revised by SN, 21-Sep-2023.)
Assertion
Ref Expression
eu6 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem eu6
StepHypRef Expression
1 dfmoeu 2530 . . . 4 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
21anbi2i 623 . . 3 ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3 abai 825 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
4 eu3v 2564 . . 3 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
52, 3, 43bitr4ri 303 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
6 abai 825 . . 3 ((∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
7 ancom 461 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8 biimpr 219 . . . . . . 7 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
98alimi 1813 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑))
109eximi 1837 . . . . 5 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝑥 = 𝑦𝜑))
11 exsbim 2005 . . . . 5 (∃𝑦𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
1210, 11syl 17 . . . 4 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
1312biantru 530 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
146, 7, 133bitr4i 302 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
155, 14bitri 274 1 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wal 1539  wex 1781  ∃!weu 2562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-ex 1782  df-nf 1786  df-mo 2534  df-eu 2563
This theorem is referenced by:  euf  2570  nfeu1  2582  dfmo  2590  sb8eulem  2592  reu6  3722  euabsn2  4729  eunex  5388  euotd  5513  iotauni  6518  iota1  6520  iotanul  6521  iotaexOLD  6523  iota4  6524  fv3  6909  eufnfv  7230  seqomlem2  8450  aceq1  10111  dfac5  10122  bnj89  33727  cbveud  36248  wl-eudf  36432  wl-euequf  36434  wl-sb8eut  36437  iotain  43166  iotaexeu  43167  iotasbc  43168  iotavalsb  43182  sbiota1  43183  eusnsn  45726  mo0sn  47490
  Copyright terms: Public domain W3C validator