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

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

Proof of Theorem eu6
StepHypRef Expression
1 dfmoeu 2611 . . . 4 ((∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
21anbi2i 622 . . 3 ((∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))) ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
3 abai 822 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑥𝜑 ∧ (∃𝑥𝜑 → ∃𝑦𝑥(𝜑𝑥 = 𝑦))))
4 eu3v 2648 . . 3 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
52, 3, 43bitr4ri 305 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)))
6 abai 822 . . 3 ((∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
7 ancom 461 . . 3 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ ∃𝑥𝜑))
8 biimpr 221 . . . . . . 7 ((𝜑𝑥 = 𝑦) → (𝑥 = 𝑦𝜑))
98alimi 1803 . . . . . 6 (∀𝑥(𝜑𝑥 = 𝑦) → ∀𝑥(𝑥 = 𝑦𝜑))
109eximi 1826 . . . . 5 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑦𝑥(𝑥 = 𝑦𝜑))
11 exsbim 1999 . . . . 5 (∃𝑦𝑥(𝑥 = 𝑦𝜑) → ∃𝑥𝜑)
1210, 11syl 17 . . . 4 (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)
1312biantru 530 . . 3 (∃𝑦𝑥(𝜑𝑥 = 𝑦) ↔ (∃𝑦𝑥(𝜑𝑥 = 𝑦) ∧ (∃𝑦𝑥(𝜑𝑥 = 𝑦) → ∃𝑥𝜑)))
146, 7, 133bitr4i 304 . 2 ((∃𝑥𝜑 ∧ ∃𝑦𝑥(𝜑𝑥 = 𝑦)) ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
155, 14bitri 276 1 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526  wex 1771  ∃!weu 2646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-10 2136  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-mo 2615  df-eu 2647
This theorem is referenced by:  euf  2654  nfeu1  2667  dfmo  2675  sb8eulem  2677  reu6  3714  euabsn2  4653  eunex  5281  euotd  5394  iotauni  6323  iota1  6325  iotanul  6326  iotaex  6328  iota4  6329  fv3  6681  eufnfv  6982  seqomlem2  8076  aceq1  9531  dfac5  9542  bnj89  31890  cbveud  34535  wl-eudf  34689  wl-euequf  34691  wl-sb8eut  34694  iotain  40626  iotaexeu  40627  iotasbc  40628  iotavalsb  40642  sbiota1  40643  eusnsn  43138
  Copyright terms: Public domain W3C validator