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

Theorem mo4 2339
Description: "At most one" expressed using implicit substitution. (Contributed by NM, 26-Jul-1995.)
Hypothesis
Ref Expression
mo4.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
mo4  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Distinct variable groups:    x, y    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem mo4
StepHypRef Expression
1 nfv 1683 . 2  |-  F/ x ps
2 mo4.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
31, 2mo4f 2338 1  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1377   E*wmo 2276
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280
This theorem is referenced by:  eu4  2340  rmo4  3296  dffun3  5599  fun11  5653  brprcneu  5859  dff13  6154  mpt2fun  6388  caovmo  6496  wemoiso  6769  wemoiso2  6770  addsrmo  9450  mulsrmo  9451  summo  13502  hausflimi  20244  vitalilem3  21782  plyexmo  22471  tglineintmo  23763  frg2wot1  24762  ajmoi  25478  pjhthmo  25924  adjmo  26455  moel  27086  prodmo  28673  funtransport  29286  funray  29395  funline  29397  lineintmo  29412
  Copyright terms: Public domain W3C validator