Theorem supeq1d 8904

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

Syntax hints:   → wi 4   = wceq 1533  supcsup 8898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-rab 3147  df-uni 4833  df-sup 8900

This theorem is referenced by:  supadd  11603  supminf  12329  rpnnen1lem6  12375  rpnnen1  12376  limsupval  14825  limsupgval  14827  gcdval  15839  gcdass  15889  pcval  16175  pceulem  16176  pceu  16177  pczpre  16178  pcdiv  16183  pcneg  16204  prmreclem1  16246  prmreclem5  16250  ramz  16355  prdsval  16722  prdsdsval  16745  prdsdsval2  16751  prdsdsval3  16752  ressprdsds  22975  xpsdsval  22985  tmsxpsval  23142  bndth  23556  elovolmr  24071  ovolctb  24085  ovoliunlem3  24099  ovolshftlem1  24104  voliunlem3  24147  voliun  24149  volsup  24151  ioorf  24168  mbfinf  24260  itg1climres  24309  itg2val  24323  itg2monolem1  24345  itg2i1fseq  24350  itg2cnlem1  24356  mdegfval  24650  mdegval  24651  mdeg0  24658  mdegvsca  24664  mdegpropd  24672  deg1val  24684  deg1mul3  24703  dgrval  24812  coe11  24837  nmoofval  28533  nmooval  28534  nmoo0  28562  nmopval  29627  nmfnval  29647  esumval  31300  esum0  31303  esumsnf  31318  esumfsupre  31325  esumsup  31343  erdszelem3  32435  erdsze  32444  elwlim  33105  ee7.2aOLD  33804  poimirlem32  34918  ovoliunnfl  34928  voliunnfl  34930  volsupnfl  34931  itg2addnc  34940  aomclem8  39654  infnsuprnmpt  41514  supsubc  41613  supxrmnf2  41699  supminfxr  41732  limsupval3  41965  limsupresre  41969  limsuplesup  41972  limsupresico  41973  limsupvaluz  41981  limsupvaluzmpt  41990  limsupvaluz2  42011  supcnvlimsup  42013  supcnvlimsupmpt  42014  limsuplt2  42026  liminfval  42032  limsupge  42034  liminfval5  42038  limsupresxr  42039  liminfresxr  42040  liminfresico  42044  limsup10ex  42046  liminflelimsuplem  42048  fourierdlem79  42463  fourierdlem96  42480  fourierdlem97  42481  fourierdlem98  42482  fourierdlem99  42483  fourierdlem105  42489  fourierdlem108  42492  fourierdlem110  42494  sge0val  42641  sge0z  42650  sge0revalmpt  42653  sge0sn  42654  sge0tsms  42655  sge0f1o  42657  sge0sup  42666  sge0resplit  42681  meaiuninclem  42755  smfsuplem2  43079  smfsup  43081  smfsupmpt  43082  smflimsuplem1  43087  smflimsuplem2  43088  smflimsuplem4  43090  smflimsuplem5  43091  smflimsuplem7  43093  smflimsup  43095