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

Theorem mo4 2313
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 1629 . 2  |-  F/ x ps
2 mo4.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
31, 2mo4f 2312 1  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359   A.wal 1549   E*wmo 2281
This theorem is referenced by:  eu4  2319  rmo4  3119  dffun3  5457  fun11  5508  brprcneu  5713  dff13  5996  wemoiso  6070  wemoiso2  6071  mpt2fun  6164  caovmo  6276  th3qlem1  7002  summo  12503  spwmo  14650  hausflimi  18004  vitalilem3  19494  plyexmo  20222  ajmoi  22352  pjhthmo  22796  adjmo  23327  prodmo  25254  funtransport  25957  funray  26066  funline  26068  lineintmo  26083  frg2wot1  28383
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285
  Copyright terms: Public domain W3C validator