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

Theorem mo4 2316
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 1754 . 2  |-  F/ x ps
2 mo4.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
31, 2mo4f 2315 1  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370   A.wal 1435   E*wmo 2267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271
This theorem is referenced by:  eu4  2317  rmo4  3270  dffun3  5612  fun11  5666  brprcneu  5874  dff13  6174  mpt2fun  6412  caovmo  6520  wemoiso  6792  wemoiso2  6793  addsrmo  9496  mulsrmo  9497  summo  13761  prodmo  13968  hausflimi  20926  vitalilem3  22445  plyexmo  23134  tglineintmo  24546  frg2wot1  25630  ajmoi  26345  pjhthmo  26790  adjmo  27320  moel  27954  funtransport  30583  funray  30692  funline  30694  lineintmo  30709  dffrege115  36211
  Copyright terms: Public domain W3C validator