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

Theorem supeq1d 7199
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 7198 . 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 1623   supcsup 7193
This theorem is referenced by:  supminf  10305  rpnnen1  10347  reexALT  10348  limsupval  11948  limsupgval  11950  rpnnen  12505  gcdval  12687  gcdass  12724  odzval  12856  pcval  12897  pceulem  12898  pceu  12899  pczpre  12900  pcdiv  12905  pcneg  12926  prmreclem1  12963  prmreclem5  12967  ramval  13055  ramz  13072  prdsval  13355  prdsdsval  13377  prdsdsval2  13383  prdsdsval3  13384  imasval  13414  imasdsval  13418  gexval  14889  ressprdsds  17935  xpsdsval  17945  tmsxpsval  18084  nmofval  18223  nmoval  18224  metdsval  18351  bndth  18456  lebnumlem1  18459  lebnumlem3  18461  ovolval  18833  elovolmr  18835  ovolctb  18849  ovoliunlem3  18863  ovolshftlem1  18868  ovolshft  18870  voliunlem3  18909  voliun  18911  volsup  18913  ioorf  18928  mbfinf  19020  mbflimsup  19021  itg1climres  19069  itg2val  19083  itg2monolem1  19105  itg2i1fseq  19110  itg2cnlem1  19116  mdegfval  19448  mdegval  19449  mdeg0  19456  mdegvsca  19462  mdegpropd  19470  deg1val  19482  deg1mul3  19501  ig1pval  19558  dgrval  19610  coe11  19634  elqaalem1  19699  elqaalem2  19700  elqaalem3  19701  elqaa  19702  nmoofval  21340  nmooval  21341  nmoo0  21369  nmopval  22436  nmfnval  22456  ballotlemi  23059  erdszelem3  23135  erdsze  23144  ee7.2aOLD  24311  pellfundval  26377  aomclem8  26571  dgraaval  26761
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-uni 3828  df-sup 7194
  Copyright terms: Public domain W3C validator