Theorem supeq1d 9420

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 9419	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	syl 18	1 ⊢ (𝜑 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  supcsup 9414

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-sup 9416

This theorem is used by:  supadd  12211  supminf  12988  rpnnen1lem6  13036  rpnnen1  13037  limsupval  15565  limsupgval  15567  gcdval  16592  gcdass  16643  pcval  16942  pceulem  16943  pceu  16944  pczpre  16945  pcdiv  16950  pcneg  16972  prmreclem1  17014  prmreclem5  17018  ramz  17123  prdsval  17546  prdsdsval  17569  prdsdsval2  17575  prdsdsval3  17576  ressprdsds  24603  xpsdsval  24613  tmsxpsval  24770  bndth  25192  elovolmr  25710  ovolctb  25724  ovoliunlem3  25738  ovolshftlem1  25743  voliunlem3  25786  voliun  25788  volsup  25790  ioorf  25807  mbfinf  25899  itg1climres  25948  itg2val  25962  itg2monolem1  25984  itg2i1fseq  25989  itg2cnlem1  25995  mdegfval  26294  mdegval  26295  mdeg0  26302  mdegvsca  26308  mdegpropd  26316  deg1val  26328  deg1mul3  26348  dgrval  26461  coe11  26486  nmoofval  31251  nmooval  31252  nmoo0  31280  nmopval  32345  nmfnval  32365  ressdeg1  33984  esumval  34564  esum0  34567  esumsnf  34582  esumfsupre  34589  esumsup  34607  erdszelem3  35780  erdsze  35789  elwlim  36408  ee7.2aOLD  37088  poimirlem32  38409  ovoliunnfl  38419  voliunnfl  38421  volsupnfl  38422  itg2addnc  38431  aomclem8  43910  infnsuprnmpt  46087  supsubc  46191  supxrmnf2  46269  supminfxr  46300  limsupval3  46528  limsupresre  46532  limsuplesup  46535  limsupresico  46536  limsupvaluz  46544  limsupvaluzmpt  46553  limsupvaluz2  46574  supcnvlimsup  46576  supcnvlimsupmpt  46577  limsuplt2  46589  liminfval  46595  limsupge  46597  liminfval5  46601  limsupresxr  46602  liminfresxr  46603  liminfresico  46607  limsup10ex  46609  liminflelimsuplem  46611  fourierdlem79  47021  fourierdlem96  47038  fourierdlem97  47039  fourierdlem98  47040  fourierdlem99  47041  fourierdlem105  47047  fourierdlem108  47050  fourierdlem110  47052  sge0val  47202  sge0z  47211  sge0revalmpt  47214  sge0sn  47215  sge0tsms  47216  sge0f1o  47218  sge0sup  47227  sge0resplit  47242  meaiuninclem  47316  smfsuplem2  47648  smfsup  47650  smfsupmpt  47651  smflimsuplem1  47656  smflimsuplem2  47657  smflimsuplem4  47659  smflimsuplem5  47660  smflimsuplem7  47662  smflimsup  47664