Theorem supeq1d 9441

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  supcsup 9435

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-sup 9437

This theorem is used by:  supadd  12288  supminf  13065  rpnnen1lem6  13113  rpnnen1  13114  limsupval  15646  limsupgval  15648  gcdval  16671  gcdass  16725  pcval  17027  pceulem  17028  pceu  17029  pczpre  17030  pcdiv  17035  pcneg  17057  prmreclem1  17099  prmreclem5  17103  ramz  17208  prdsval  17631  prdsdsval  17654  prdsdsval2  17660  prdsdsval3  17661  ressprdsds  24695  xpsdsval  24705  tmsxpsval  24862  bndth  25284  elovolmr  25802  ovolctb  25816  ovoliunlem3  25830  ovolshftlem1  25835  voliunlem3  25878  voliun  25880  volsup  25882  ioorf  25899  mbfinf  25991  itg1climres  26040  itg2val  26054  itg2monolem1  26076  itg2i1fseq  26081  itg2cnlem1  26087  mdegfval  26385  mdegval  26386  mdeg0  26393  mdegvsca  26399  mdegpropd  26407  deg1val  26419  deg1mul3  26439  dgrval  26552  coe11  26577  nmoofval  31369  nmooval  31370  nmoo0  31398  nmopval  32463  nmfnval  32483  ressdeg1  34144  esumval  34724  esum0  34727  esumsnf  34742  esumfsupre  34749  esumsup  34767  erdszelem3  36044  erdsze  36053  elwlim  36677  ee7.2aOLD  37341  poimirlem32  38663  ovoliunnfl  38673  voliunnfl  38675  volsupnfl  38676  itg2addnc  38685  aomclem8  44156  infnsuprnmpt  46355  supsubc  46458  supxrmnf2  46536  supminfxr  46567  limsupval3  46795  limsupresre  46799  limsuplesup  46802  limsupresico  46803  limsupvaluz  46811  limsupvaluzmpt  46820  limsupvaluz2  46841  supcnvlimsup  46843  supcnvlimsupmpt  46844  limsuplt2  46856  liminfval  46862  limsupge  46864  liminfval5  46868  limsupresxr  46869  liminfresxr  46870  liminfresico  46874  limsup10ex  46876  liminflelimsuplem  46878  fourierdlem79  47288  fourierdlem96  47305  fourierdlem97  47306  fourierdlem98  47307  fourierdlem99  47308  fourierdlem105  47314  fourierdlem108  47317  fourierdlem110  47319  sge0val  47469  sge0z  47478  sge0revalmpt  47481  sge0sn  47482  sge0tsms  47483  sge0f1o  47485  sge0sup  47494  sge0resplit  47509  meaiuninclem  47583  smfsuplem2  47915  smfsup  47917  smfsupmpt  47918  smflimsuplem1  47923  smflimsuplem2  47924  smflimsuplem4  47926  smflimsuplem5  47927  smflimsuplem7  47929  smflimsup  47931