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

Theorem eu4 2547
 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 2524 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2 eu4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32mo4 2546 . . 3 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 730 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 264 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383  ∀wal 1521  ∃wex 1744  ∃!weu 2498  ∃*wmo 2499 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503 This theorem is referenced by:  eueq  3411  euind  3426  eqeuel  3974  uniintsn  4546  eusv1  4890  omeu  7710  eroveu  7885  climeu  14330  pceu  15598  initoeu2lem2  16712  psgneu  17972  gsumval3eu  18351  frgr3vlem2  27254  3vfriswmgrlem  27257  unirep  33637  rlimdmafv  41578
 Copyright terms: Public domain W3C validator