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

Theorem mo4 2504
Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
mo4.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
mo4 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Distinct variable groups:   𝑥,𝑦   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem mo4
StepHypRef Expression
1 nfv 1829 . 2 𝑥𝜓
2 mo4.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2mo4f 2503 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  wal 1472  ∃*wmo 2458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233
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 1867  df-eu 2461  df-mo 2462
This theorem is referenced by:  eu4  2505  rmo4  3365  dffun3  5800  fun11  5862  brprcneu  6080  dff13  6393  mpt2fun  6637  caovmo  6746  wemoiso  7021  wemoiso2  7022  addsrmo  9750  mulsrmo  9751  summo  14243  prodmo  14453  hausflimi  21541  vitalilem3  23129  plyexmo  23816  tglineintmo  25282  frg2wot1  26377  ajmoi  26891  pjhthmo  27338  adjmo  27868  moel  28500  funtransport  31101  funray  31210  funline  31212  lineintmo  31227  dffrege115  37075  frgr2wwlk1  41475
  Copyright terms: Public domain W3C validator