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

Theorem eu4 2692
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 df-eu 2647 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2 eu4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32mo4 2643 . . 3 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 622 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 276 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1526  wex 1771  ∃*wmo 2613  ∃!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
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-mo 2615  df-eu 2647
This theorem is referenced by:  euind  3712  eqeuel  4319  uniintsn  4904  eusv1  5282  omeu  8200  eroveu  8381  climeu  14900  pceu  16171  initoeu2lem2  17263  psgneu  18563  gsumval3eu  18953  frgr3vlem2  27980  3vfriswmgrlem  27983  unirep  34869  rlimdmafv  43253  rlimdmafv2  43334
  Copyright terms: Public domain W3C validator