Theorem supeq1d 9330

Description: Equality deduction for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1d.1	⊢ (𝜑 → 𝐵 = 𝐶)

Assertion

Ref	Expression
supeq1d	⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Proof of Theorem supeq1d

Step	Hyp	Ref	Expression
1		supeq1d.1	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
2		supeq1 9329	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	syl 17	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

Syntax hints:   → wi 4   = wceq 1541  supcsup 9324

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-uni 4860  df-sup 9326

This theorem is referenced by:  supadd  12090  supminf  12833  rpnnen1lem6  12880  rpnnen1  12881  limsupval  15381  limsupgval  15383  gcdval  16407  gcdass  16458  pcval  16756  pceulem  16757  pceu  16758  pczpre  16759  pcdiv  16764  pcneg  16786  prmreclem1  16828  prmreclem5  16832  ramz  16937  prdsval  17359  prdsdsval  17382  prdsdsval2  17388  prdsdsval3  17389  ressprdsds  24287  xpsdsval  24297  tmsxpsval  24454  bndth  24885  elovolmr  25405  ovolctb  25419  ovoliunlem3  25433  ovolshftlem1  25438  voliunlem3  25481  voliun  25483  volsup  25485  ioorf  25502  mbfinf  25594  itg1climres  25643  itg2val  25657  itg2monolem1  25679  itg2i1fseq  25684  itg2cnlem1  25690  mdegfval  25995  mdegval  25996  mdeg0  26003  mdegvsca  26009  mdegpropd  26017  deg1val  26029  deg1mul3  26049  dgrval  26161  coe11  26186  nmoofval  30740  nmooval  30741  nmoo0  30769  nmopval  31834  nmfnval  31854  ressdeg1  33527  esumval  34057  esum0  34060  esumsnf  34075  esumfsupre  34082  esumsup  34100  erdszelem3  35235  erdsze  35244  elwlim  35863  ee7.2aOLD  36501  poimirlem32  37698  ovoliunnfl  37708  voliunnfl  37710  volsupnfl  37711  itg2addnc  37720  aomclem8  43100  infnsuprnmpt  45293  supsubc  45398  supxrmnf2  45477  supminfxr  45508  limsupval3  45736  limsupresre  45740  limsuplesup  45743  limsupresico  45744  limsupvaluz  45752  limsupvaluzmpt  45761  limsupvaluz2  45782  supcnvlimsup  45784  supcnvlimsupmpt  45785  limsuplt2  45797  liminfval  45803  limsupge  45805  liminfval5  45809  limsupresxr  45810  liminfresxr  45811  liminfresico  45815  limsup10ex  45817  liminflelimsuplem  45819  fourierdlem79  46229  fourierdlem96  46246  fourierdlem97  46247  fourierdlem98  46248  fourierdlem99  46249  fourierdlem105  46255  fourierdlem108  46258  fourierdlem110  46260  sge0val  46410  sge0z  46419  sge0revalmpt  46422  sge0sn  46423  sge0tsms  46424  sge0f1o  46426  sge0sup  46435  sge0resplit  46450  meaiuninclem  46524  smfsuplem2  46856  smfsup  46858  smfsupmpt  46859  smflimsuplem1  46864  smflimsuplem2  46865  smflimsuplem4  46867  smflimsuplem5  46868  smflimsuplem7  46870  smflimsup  46872