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

Theorem eu4 2517
Description: Uniqueness using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
eu4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
eu4 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem eu4
StepHypRef Expression
1 eu5 2495 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2 eu4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32mo4 2516 . . 3 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 730 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 264 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  wal 1480  wex 1703  ∃!weu 2469  ∃*wmo 2470
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474
This theorem is referenced by:  eueq  3376  euind  3391  eqeuel  3939  uniintsn  4512  eusv1  4858  omeu  7662  eroveu  7839  climeu  14280  pceu  15545  initoeu2lem2  16659  psgneu  17920  gsumval3eu  18299  frgr3vlem2  27131  3vfriswmgrlem  27134  unirep  33487  rlimdmafv  41026
  Copyright terms: Public domain W3C validator