Theorem supeq1d 9515

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

Syntax hints:   → wi 4   = wceq 1537  supcsup 9509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-ss 3993  df-uni 4932  df-sup 9511

This theorem is referenced by:  supadd  12263  supminf  13000  rpnnen1lem6  13047  rpnnen1  13048  limsupval  15520  limsupgval  15522  gcdval  16542  gcdass  16594  pcval  16891  pceulem  16892  pceu  16893  pczpre  16894  pcdiv  16899  pcneg  16921  prmreclem1  16963  prmreclem5  16967  ramz  17072  prdsval  17515  prdsdsval  17538  prdsdsval2  17544  prdsdsval3  17545  ressprdsds  24402  xpsdsval  24412  tmsxpsval  24572  bndth  25009  elovolmr  25530  ovolctb  25544  ovoliunlem3  25558  ovolshftlem1  25563  voliunlem3  25606  voliun  25608  volsup  25610  ioorf  25627  mbfinf  25719  itg1climres  25769  itg2val  25783  itg2monolem1  25805  itg2i1fseq  25810  itg2cnlem1  25816  mdegfval  26121  mdegval  26122  mdeg0  26129  mdegvsca  26135  mdegpropd  26143  deg1val  26155  deg1mul3  26175  dgrval  26287  coe11  26312  nmoofval  30794  nmooval  30795  nmoo0  30823  nmopval  31888  nmfnval  31908  ressdeg1  33556  esumval  34010  esum0  34013  esumsnf  34028  esumfsupre  34035  esumsup  34053  erdszelem3  35161  erdsze  35170  elwlim  35787  ee7.2aOLD  36427  poimirlem32  37612  ovoliunnfl  37622  voliunnfl  37624  volsupnfl  37625  itg2addnc  37634  aomclem8  43018  infnsuprnmpt  45159  supsubc  45268  supxrmnf2  45348  supminfxr  45379  limsupval3  45613  limsupresre  45617  limsuplesup  45620  limsupresico  45621  limsupvaluz  45629  limsupvaluzmpt  45638  limsupvaluz2  45659  supcnvlimsup  45661  supcnvlimsupmpt  45662  limsuplt2  45674  liminfval  45680  limsupge  45682  liminfval5  45686  limsupresxr  45687  liminfresxr  45688  liminfresico  45692  limsup10ex  45694  liminflelimsuplem  45696  fourierdlem79  46106  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem105  46132  fourierdlem108  46135  fourierdlem110  46137  sge0val  46287  sge0z  46296  sge0revalmpt  46299  sge0sn  46300  sge0tsms  46301  sge0f1o  46303  sge0sup  46312  sge0resplit  46327  meaiuninclem  46401  smfsuplem2  46733  smfsup  46735  smfsupmpt  46736  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem4  46744  smflimsuplem5  46745  smflimsuplem7  46747  smflimsup  46749