Theorem supeq1d 9352

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

Syntax hints:   → wi 4   = wceq 1542  supcsup 9346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-ss 3907  df-uni 4852  df-sup 9348

This theorem is referenced by:  supadd  12115  supminf  12876  rpnnen1lem6  12923  rpnnen1  12924  limsupval  15427  limsupgval  15429  gcdval  16456  gcdass  16507  pcval  16806  pceulem  16807  pceu  16808  pczpre  16809  pcdiv  16814  pcneg  16836  prmreclem1  16878  prmreclem5  16882  ramz  16987  prdsval  17409  prdsdsval  17432  prdsdsval2  17438  prdsdsval3  17439  ressprdsds  24346  xpsdsval  24356  tmsxpsval  24513  bndth  24935  elovolmr  25453  ovolctb  25467  ovoliunlem3  25481  ovolshftlem1  25486  voliunlem3  25529  voliun  25531  volsup  25533  ioorf  25550  mbfinf  25642  itg1climres  25691  itg2val  25705  itg2monolem1  25727  itg2i1fseq  25732  itg2cnlem1  25738  mdegfval  26037  mdegval  26038  mdeg0  26045  mdegvsca  26051  mdegpropd  26059  deg1val  26071  deg1mul3  26091  dgrval  26203  coe11  26228  nmoofval  30848  nmooval  30849  nmoo0  30877  nmopval  31942  nmfnval  31962  ressdeg1  33641  esumval  34206  esum0  34209  esumsnf  34224  esumfsupre  34231  esumsup  34249  erdszelem3  35391  erdsze  35400  elwlim  36019  ee7.2aOLD  36659  poimirlem32  37987  ovoliunnfl  37997  voliunnfl  37999  volsupnfl  38000  itg2addnc  38009  aomclem8  43507  infnsuprnmpt  45697  supsubc  45801  supxrmnf2  45879  supminfxr  45910  limsupval3  46138  limsupresre  46142  limsuplesup  46145  limsupresico  46146  limsupvaluz  46154  limsupvaluzmpt  46163  limsupvaluz2  46184  supcnvlimsup  46186  supcnvlimsupmpt  46187  limsuplt2  46199  liminfval  46205  limsupge  46207  liminfval5  46211  limsupresxr  46212  liminfresxr  46213  liminfresico  46217  limsup10ex  46219  liminflelimsuplem  46221  fourierdlem79  46631  fourierdlem96  46648  fourierdlem97  46649  fourierdlem98  46650  fourierdlem99  46651  fourierdlem105  46657  fourierdlem108  46660  fourierdlem110  46662  sge0val  46812  sge0z  46821  sge0revalmpt  46824  sge0sn  46825  sge0tsms  46826  sge0f1o  46828  sge0sup  46837  sge0resplit  46852  meaiuninclem  46926  smfsuplem2  47258  smfsup  47260  smfsupmpt  47261  smflimsuplem1  47266  smflimsuplem2  47267  smflimsuplem4  47269  smflimsuplem5  47270  smflimsuplem7  47272  smflimsup  47274