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

Theorem eu4 2501
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 2479 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2 eu4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32mo4 2500 . . 3 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 725 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 262 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472  wex 1694  ∃!weu 2453  ∃*wmo 2454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458
This theorem is referenced by:  eueq  3340  euind  3355  uniintsn  4439  eusv1  4777  omeu  7525  eroveu  7702  climeu  14076  pceu  15331  initoeu2lem2  16430  psgneu  17691  gsumval3eu  18070  frgra3vlem2  26290  3vfriswmgralem  26293  frg2woteqm  26348  unirep  32476  rlimdmafv  39707  frgr3vlem2  41442  3vfriswmgrlem  41445
  Copyright terms: Public domain W3C validator