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 1673 . 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 184    /\ wa 369   A.wal 1367   E*wmo 2254
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258
This theorem is referenced by:  eu4  2318  rmo4  3150  dffun3  5427  fun11  5481  brprcneu  5682  dff13  5969  mpt2fun  6190  caovmo  6298  wemoiso  6560  wemoiso2  6561  th3qlem1  7204  summo  13192  hausflimi  19551  vitalilem3  21088  plyexmo  21777  tglineintmo  23045  ajmoi  24257  pjhthmo  24703  adjmo  25234  moel  25865  prodmo  27447  funtransport  28060  funray  28169  funline  28171  lineintmo  28186  frg2wot1  30647
  Copyright terms: Public domain W3C validator