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

Theorem supeq1d 7454
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 7453 . 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 1653   supcsup 7448
This theorem is referenced by:  supminf  10568  rpnnen1  10610  reexALT  10611  limsupval  12273  limsupgval  12275  rpnnen  12831  gcdval  13013  gcdass  13050  odzval  13182  pcval  13223  pceulem  13224  pceu  13225  pczpre  13226  pcdiv  13231  pcneg  13252  prmreclem1  13289  prmreclem5  13293  ramval  13381  ramz  13398  prdsval  13683  prdsdsval  13705  prdsdsval2  13711  prdsdsval3  13712  imasval  13742  imasdsval  13746  gexval  15217  ressprdsds  18406  xpsdsval  18416  tmsxpsval  18573  nmofval  18753  nmoval  18754  metdsval  18882  bndth  18988  lebnumlem1  18991  lebnumlem3  18993  ovolval  19375  elovolmr  19377  ovolctb  19391  ovoliunlem3  19405  ovolshftlem1  19410  ovolshft  19412  voliunlem3  19451  voliun  19453  volsup  19455  ioorf  19470  mbfinf  19560  mbflimsup  19561  itg1climres  19609  itg2val  19623  itg2monolem1  19645  itg2i1fseq  19650  itg2cnlem1  19656  mdegfval  19990  mdegval  19991  mdeg0  19998  mdegvsca  20004  mdegpropd  20012  deg1val  20024  deg1mul3  20043  ig1pval  20100  dgrval  20152  coe11  20176  elqaalem1  20241  elqaalem2  20242  elqaalem3  20243  elqaa  20244  nmoofval  22268  nmooval  22269  nmoo0  22297  nmopval  23364  nmfnval  23384  esumval  24446  esum0  24449  esumsn  24461  esumfsupre  24466  ballotlemi  24763  erdszelem3  24884  erdsze  24893  elwlim  25579  ee7.2aOLD  26216  supadd  26246  ovoliunnfl  26259  voliunnfl  26261  volsupnfl  26262  itg2addnc  26272  pellfundval  26956  aomclem8  27149  dgraaval  27339
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2712  df-rex 2713  df-rab 2716  df-uni 4018  df-sup 7449
  Copyright terms: Public domain W3C validator