Theorem supeq1d 9135

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

Syntax hints:   → wi 4   = wceq 1539  supcsup 9129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-sup 9131

This theorem is referenced by:  supadd  11873  supminf  12604  rpnnen1lem6  12651  rpnnen1  12652  limsupval  15111  limsupgval  15113  gcdval  16131  gcdass  16183  pcval  16473  pceulem  16474  pceu  16475  pczpre  16476  pcdiv  16481  pcneg  16503  prmreclem1  16545  prmreclem5  16549  ramz  16654  prdsval  17083  prdsdsval  17106  prdsdsval2  17112  prdsdsval3  17113  ressprdsds  23432  xpsdsval  23442  tmsxpsval  23600  bndth  24027  elovolmr  24545  ovolctb  24559  ovoliunlem3  24573  ovolshftlem1  24578  voliunlem3  24621  voliun  24623  volsup  24625  ioorf  24642  mbfinf  24734  itg1climres  24784  itg2val  24798  itg2monolem1  24820  itg2i1fseq  24825  itg2cnlem1  24831  mdegfval  25132  mdegval  25133  mdeg0  25140  mdegvsca  25146  mdegpropd  25154  deg1val  25166  deg1mul3  25185  dgrval  25294  coe11  25319  nmoofval  29025  nmooval  29026  nmoo0  29054  nmopval  30119  nmfnval  30139  esumval  31914  esum0  31917  esumsnf  31932  esumfsupre  31939  esumsup  31957  erdszelem3  33055  erdsze  33064  elwlim  33744  ee7.2aOLD  34577  poimirlem32  35736  ovoliunnfl  35746  voliunnfl  35748  volsupnfl  35749  itg2addnc  35758  aomclem8  40802  infnsuprnmpt  42685  supsubc  42782  supxrmnf2  42863  supminfxr  42894  limsupval3  43123  limsupresre  43127  limsuplesup  43130  limsupresico  43131  limsupvaluz  43139  limsupvaluzmpt  43148  limsupvaluz2  43169  supcnvlimsup  43171  supcnvlimsupmpt  43172  limsuplt2  43184  liminfval  43190  limsupge  43192  liminfval5  43196  limsupresxr  43197  liminfresxr  43198  liminfresico  43202  limsup10ex  43204  liminflelimsuplem  43206  fourierdlem79  43616  fourierdlem96  43633  fourierdlem97  43634  fourierdlem98  43635  fourierdlem99  43636  fourierdlem105  43642  fourierdlem108  43645  fourierdlem110  43647  sge0val  43794  sge0z  43803  sge0revalmpt  43806  sge0sn  43807  sge0tsms  43808  sge0f1o  43810  sge0sup  43819  sge0resplit  43834  meaiuninclem  43908  smfsuplem2  44232  smfsup  44234  smfsupmpt  44235  smflimsuplem1  44240  smflimsuplem2  44241  smflimsuplem4  44243  smflimsuplem5  44244  smflimsuplem7  44246  smflimsup  44248