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

Theorem supeq1d 7386
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 7385 . 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 1649   supcsup 7380
This theorem is referenced by:  supminf  10495  rpnnen1  10537  reexALT  10538  limsupval  12195  limsupgval  12197  rpnnen  12753  gcdval  12935  gcdass  12972  odzval  13104  pcval  13145  pceulem  13146  pceu  13147  pczpre  13148  pcdiv  13153  pcneg  13174  prmreclem1  13211  prmreclem5  13215  ramval  13303  ramz  13320  prdsval  13605  prdsdsval  13627  prdsdsval2  13633  prdsdsval3  13634  imasval  13664  imasdsval  13668  gexval  15139  ressprdsds  18309  xpsdsval  18319  tmsxpsval  18458  nmofval  18619  nmoval  18620  metdsval  18748  bndth  18854  lebnumlem1  18857  lebnumlem3  18859  ovolval  19237  elovolmr  19239  ovolctb  19253  ovoliunlem3  19267  ovolshftlem1  19272  ovolshft  19274  voliunlem3  19313  voliun  19315  volsup  19317  ioorf  19332  mbfinf  19424  mbflimsup  19425  itg1climres  19473  itg2val  19487  itg2monolem1  19509  itg2i1fseq  19514  itg2cnlem1  19520  mdegfval  19852  mdegval  19853  mdeg0  19860  mdegvsca  19866  mdegpropd  19874  deg1val  19886  deg1mul3  19905  ig1pval  19962  dgrval  20014  coe11  20038  elqaalem1  20103  elqaalem2  20104  elqaalem3  20105  elqaa  20106  nmoofval  22111  nmooval  22112  nmoo0  22140  nmopval  23207  nmfnval  23227  esumval  24237  esum0  24240  esumsn  24252  esumfsupre  24257  ballotlemi  24537  erdszelem3  24658  erdsze  24667  ee7.2aOLD  25925  supadd  25948  ovoliunnfl  25953  voliunnfl  25955  volsupnfl  25956  itg2addnc  25959  pellfundval  26634  aomclem8  26828  dgraaval  27018
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ral 2654  df-rex 2655  df-rab 2658  df-uni 3958  df-sup 7381
  Copyright terms: Public domain W3C validator