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

Theorem mo4 2505
 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 1830 . 2 𝑥𝜓
2 mo4.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2mo4f 2504 1 (∃*𝑥𝜑 ↔ ∀𝑥𝑦((𝜑𝜓) → 𝑥 = 𝑦))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473  ∃*wmo 2459 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463 This theorem is referenced by:  eu4  2506  rmo4  3366  dffun3  5815  fun11  5877  brprcneu  6096  dff13  6416  mpt2fun  6660  caovmo  6769  wemoiso  7044  wemoiso2  7045  addsrmo  9773  mulsrmo  9774  summo  14295  prodmo  14505  hausflimi  21594  vitalilem3  23185  plyexmo  23872  tglineintmo  25337  frg2wot1  26584  ajmoi  27098  pjhthmo  27545  adjmo  28075  moel  28707  funtransport  31308  funray  31417  funline  31419  lineintmo  31434  dffrege115  37292  frgr2wwlk1  41494
 Copyright terms: Public domain W3C validator