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

Theorem supeq1d 7442
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 7441 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2syl 16 1  |-  ( ph  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652   supcsup 7436
This theorem is referenced by:  supminf  10552  rpnnen1  10594  reexALT  10595  limsupval  12256  limsupgval  12258  rpnnen  12814  gcdval  12996  gcdass  13033  odzval  13165  pcval  13206  pceulem  13207  pceu  13208  pczpre  13209  pcdiv  13214  pcneg  13235  prmreclem1  13272  prmreclem5  13276  ramval  13364  ramz  13381  prdsval  13666  prdsdsval  13688  prdsdsval2  13694  prdsdsval3  13695  imasval  13725  imasdsval  13729  gexval  15200  ressprdsds  18389  xpsdsval  18399  tmsxpsval  18556  nmofval  18736  nmoval  18737  metdsval  18865  bndth  18971  lebnumlem1  18974  lebnumlem3  18976  ovolval  19358  elovolmr  19360  ovolctb  19374  ovoliunlem3  19388  ovolshftlem1  19393  ovolshft  19395  voliunlem3  19434  voliun  19436  volsup  19438  ioorf  19453  mbfinf  19545  mbflimsup  19546  itg1climres  19594  itg2val  19608  itg2monolem1  19630  itg2i1fseq  19635  itg2cnlem1  19641  mdegfval  19973  mdegval  19974  mdeg0  19981  mdegvsca  19987  mdegpropd  19995  deg1val  20007  deg1mul3  20026  ig1pval  20083  dgrval  20135  coe11  20159  elqaalem1  20224  elqaalem2  20225  elqaalem3  20226  elqaa  20227  nmoofval  22251  nmooval  22252  nmoo0  22280  nmopval  23347  nmfnval  23367  esumval  24429  esum0  24432  esumsn  24444  esumfsupre  24449  ballotlemi  24746  erdszelem3  24867  erdsze  24876  ee7.2aOLD  26159  supadd  26185  ovoliunnfl  26194  voliunnfl  26196  volsupnfl  26197  itg2addnc  26205  pellfundval  26880  aomclem8  27074  dgraaval  27264
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  ax-ext 2416
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-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ral 2702  df-rex 2703  df-rab 2706  df-uni 4008  df-sup 7437
  Copyright terms: Public domain W3C validator