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

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

Proof of Theorem eu6
StepHypRef Expression
1 dfmoeu 2531 . . . 4 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
21anbi2i 624 . . 3 ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3 abai 826 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
4 eu3v 2565 . . 3 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
52, 3, 43bitr4ri 304 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
6 abai 826 . . 3 ((∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
7 ancom 462 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8 biimpr 219 . . . . . . 7 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
98alimi 1814 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑))
109eximi 1838 . . . . 5 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝑥 = 𝑦𝜑))
11 exsbim 2006 . . . . 5 (∃𝑦𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
1210, 11syl 17 . . . 4 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
1312biantru 531 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
146, 7, 133bitr4i 303 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
155, 14bitri 275 1 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  wal 1540  wex 1782  ∃!weu 2563
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2138  ax-12 2172
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-ex 1783  df-nf 1787  df-mo 2535  df-eu 2564
This theorem is referenced by:  euf  2571  nfeu1  2583  dfmo  2591  sb8eulem  2593  reu6  3723  euabsn2  4730  eunex  5389  euotd  5514  iotauni  6519  iota1  6521  iotanul  6522  iotaexOLD  6524  iota4  6525  fv3  6910  eufnfv  7231  seqomlem2  8451  aceq1  10112  dfac5  10123  bnj89  33732  cbveud  36253  wl-eudf  36437  wl-euequf  36439  wl-sb8eut  36442  iotain  43176  iotaexeu  43177  iotasbc  43178  iotavalsb  43192  sbiota1  43193  eusnsn  45736  mo0sn  47500
  Copyright terms: Public domain W3C validator