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

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

Proof of Theorem eu6
StepHypRef Expression
1 dfmoeu 2536 . . . 4 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
21anbi2i 623 . . 3 ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3 abai 827 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
4 eu3v 2570 . . 3 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
52, 3, 43bitr4ri 304 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
6 abai 827 . . 3 ((∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
7 ancom 460 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8 biimpr 220 . . . . . . 7 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
98alimi 1811 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑))
109eximi 1835 . . . . 5 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝑥 = 𝑦𝜑))
11 exsbim 2001 . . . . 5 (∃𝑦𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
1210, 11syl 17 . . . 4 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
1312biantru 529 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
146, 7, 133bitr4i 303 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
155, 14bitri 275 1 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wal 1538  wex 1779  ∃!weu 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-mo 2540  df-eu 2569
This theorem is referenced by:  euf  2576  nfeu1  2588  dfmo  2596  sb8eulem  2598  reu6  3732  euabsn2  4725  eunex  5390  euotd  5518  iotauni  6536  iota1  6538  iotanul  6539  iotaexOLD  6541  iota4  6542  fv3  6924  eufnfv  7249  seqomlem2  8491  aceq1  10157  dfac5  10169  bnj89  34735  cbveud  37373  wl-eudf  37573  wl-euequf  37575  wl-sb8eut  37579  wl-sb8eutv  37580  iotain  44436  iotaexeu  44437  iotasbc  44438  iotavalsb  44452  sbiota1  44453  dfac5prim  45007  eusnsn  47038  mo0sn  48735
  Copyright terms: Public domain W3C validator