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

Theorem eu4 2696
 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 2649 . 2 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2 eu4.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
32mo4 2645 . . 3 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
43anbi2i 622 . 2 ((∃𝑥𝜑 ∧ ∃*𝑥𝜑) ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
51, 4bitri 276 1 (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396  ∀wal 1528  ∃wex 1773  ∃*wmo 2613  ∃!weu 2648 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008 This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-mo 2615  df-eu 2649 This theorem is referenced by:  euind  3718  eqeuel  4325  uniintsn  4910  eusv1  5287  omeu  8204  eroveu  8385  climeu  14905  pceu  16175  initoeu2lem2  17267  psgneu  18556  gsumval3eu  18946  frgr3vlem2  27968  3vfriswmgrlem  27971  unirep  34857  rlimdmafv  43239  rlimdmafv2  43320
 Copyright terms: Public domain W3C validator