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

Theorem mo4 2317
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 1756 . 2  |-  F/ x ps
2 mo4.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
31, 2mo4f 2316 1  |-  ( E* x ph  <->  A. x A. y ( ( ph  /\ 
ps )  ->  x  =  y ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371   A.wal 1436   E*wmo 2271
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-eu 2274  df-mo 2275
This theorem is referenced by:  eu4  2318  rmo4  3269  dffun3  5618  fun11  5672  brprcneu  5880  dff13  6180  mpt2fun  6418  caovmo  6526  wemoiso  6798  wemoiso2  6799  addsrmo  9510  mulsrmo  9511  summo  13788  prodmo  13995  hausflimi  20999  vitalilem3  22572  plyexmo  23270  tglineintmo  24691  frg2wot1  25789  ajmoi  26504  pjhthmo  26959  adjmo  27489  moel  28123  funtransport  30809  funray  30918  funline  30920  lineintmo  30935  dffrege115  36550
  Copyright terms: Public domain W3C validator