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

Theorem supeq1d 7215
Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)
Hypothesis
Ref Expression
supeq1d.1  |-  ( ph  ->  B  =  C )
Assertion
Ref Expression
supeq1d  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)

Proof of Theorem supeq1d
StepHypRef Expression
1 supeq1d.1 . 2  |-  ( ph  ->  B  =  C )
2 supeq1 7214 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2syl 15 1  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632   supcsup 7209
This theorem is referenced by:  supminf  10321  rpnnen1  10363  reexALT  10364  limsupval  11964  limsupgval  11966  rpnnen  12521  gcdval  12703  gcdass  12740  odzval  12872  pcval  12913  pceulem  12914  pceu  12915  pczpre  12916  pcdiv  12921  pcneg  12942  prmreclem1  12979  prmreclem5  12983  ramval  13071  ramz  13088  prdsval  13371  prdsdsval  13393  prdsdsval2  13399  prdsdsval3  13400  imasval  13430  imasdsval  13434  gexval  14905  ressprdsds  17951  xpsdsval  17961  tmsxpsval  18100  nmofval  18239  nmoval  18240  metdsval  18367  bndth  18472  lebnumlem1  18475  lebnumlem3  18477  ovolval  18849  elovolmr  18851  ovolctb  18865  ovoliunlem3  18879  ovolshftlem1  18884  ovolshft  18886  voliunlem3  18925  voliun  18927  volsup  18929  ioorf  18944  mbfinf  19036  mbflimsup  19037  itg1climres  19085  itg2val  19099  itg2monolem1  19121  itg2i1fseq  19126  itg2cnlem1  19132  mdegfval  19464  mdegval  19465  mdeg0  19472  mdegvsca  19478  mdegpropd  19486  deg1val  19498  deg1mul3  19517  ig1pval  19574  dgrval  19626  coe11  19650  elqaalem1  19715  elqaalem2  19716  elqaalem3  19717  elqaa  19718  nmoofval  21356  nmooval  21357  nmoo0  21385  nmopval  22452  nmfnval  22472  ballotlemi  23075  esumval  23440  esum0  23443  esumsn  23452  erdszelem3  23739  erdsze  23748  ee7.2aOLD  24972  supadd  24996  ovoliunnfl  25001  itg2addnc  25005  pellfundval  27068  aomclem8  27262  dgraaval  27452
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ral 2561  df-rex 2562  df-rab 2565  df-uni 3844  df-sup 7210
  Copyright terms: Public domain W3C validator