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

Theorem mo4 2337
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:   ,   ,   ,

Proof of Theorem mo4
StepHypRef Expression
1 nfv 1707 . 2
2 mo4.1 . 2
31, 2mo4f 2336 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  A.wal 1393  E*wmo 2283
This theorem is referenced by:  eu4  2338  rmo4  3292  dffun3  5604  fun11  5658  brprcneu  5864  dff13  6166  mpt2fun  6404  caovmo  6512  wemoiso  6785  wemoiso2  6786  addsrmo  9471  mulsrmo  9472  summo  13539  prodmo  13743  hausflimi  20481  vitalilem3  22019  plyexmo  22709  tglineintmo  24022  frg2wot1  25057  ajmoi  25774  pjhthmo  26220  adjmo  26751  moel  27382  funtransport  29681  funray  29790  funline  29792  lineintmo  29807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287
  Copyright terms: Public domain W3C validator