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

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

Proof of Theorem eu6
StepHypRef Expression
1 dfmoeu 2597 . . . 4 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
21anbi2i 625 . . 3 ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3 abai 825 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
4 eu3v 2633 . . 3 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
52, 3, 43bitr4ri 307 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
6 abai 825 . . 3 ((∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
7 ancom 464 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8 biimpr 223 . . . . . . 7 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
98alimi 1813 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑))
109eximi 1836 . . . . 5 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝑥 = 𝑦𝜑))
11 exsbim 2008 . . . . 5 (∃𝑦𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
1210, 11syl 17 . . . 4 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
1312biantru 533 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
146, 7, 133bitr4i 306 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
155, 14bitri 278 1 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  wal 1536  wex 1781  ∃!weu 2631
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 1911  ax-6 1970  ax-7 2015  ax-10 2143  ax-12 2176
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-mo 2601  df-eu 2632
This theorem is referenced by:  euf  2639  nfeu1  2652  dfmo  2660  sb8eulem  2662  reu6  3668  euabsn2  4624  eunex  5259  euotd  5371  iotauni  6303  iota1  6305  iotanul  6306  iotaex  6308  iota4  6309  fv3  6667  eufnfv  6973  seqomlem2  8074  aceq1  9532  dfac5  9543  bnj89  32105  cbveud  34790  wl-eudf  34972  wl-euequf  34974  wl-sb8eut  34977  iotain  41114  iotaexeu  41115  iotasbc  41116  iotavalsb  41130  sbiota1  41131  eusnsn  43611
  Copyright terms: Public domain W3C validator