Theorem supeq1d 9355

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

Syntax hints:   → wi 4   = wceq 1540  supcsup 9349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-ss 3922  df-uni 4862  df-sup 9351

This theorem is referenced by:  supadd  12111  supminf  12854  rpnnen1lem6  12901  rpnnen1  12902  limsupval  15399  limsupgval  15401  gcdval  16425  gcdass  16476  pcval  16774  pceulem  16775  pceu  16776  pczpre  16777  pcdiv  16782  pcneg  16804  prmreclem1  16846  prmreclem5  16850  ramz  16955  prdsval  17377  prdsdsval  17400  prdsdsval2  17406  prdsdsval3  17407  ressprdsds  24275  xpsdsval  24285  tmsxpsval  24442  bndth  24873  elovolmr  25393  ovolctb  25407  ovoliunlem3  25421  ovolshftlem1  25426  voliunlem3  25469  voliun  25471  volsup  25473  ioorf  25490  mbfinf  25582  itg1climres  25631  itg2val  25645  itg2monolem1  25667  itg2i1fseq  25672  itg2cnlem1  25678  mdegfval  25983  mdegval  25984  mdeg0  25991  mdegvsca  25997  mdegpropd  26005  deg1val  26017  deg1mul3  26037  dgrval  26149  coe11  26174  nmoofval  30724  nmooval  30725  nmoo0  30753  nmopval  31818  nmfnval  31838  ressdeg1  33514  esumval  34015  esum0  34018  esumsnf  34033  esumfsupre  34040  esumsup  34058  erdszelem3  35168  erdsze  35177  elwlim  35799  ee7.2aOLD  36437  poimirlem32  37634  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  itg2addnc  37656  aomclem8  43037  infnsuprnmpt  45231  supsubc  45336  supxrmnf2  45416  supminfxr  45447  limsupval3  45677  limsupresre  45681  limsuplesup  45684  limsupresico  45685  limsupvaluz  45693  limsupvaluzmpt  45702  limsupvaluz2  45723  supcnvlimsup  45725  supcnvlimsupmpt  45726  limsuplt2  45738  liminfval  45744  limsupge  45746  liminfval5  45750  limsupresxr  45751  liminfresxr  45752  liminfresico  45756  limsup10ex  45758  liminflelimsuplem  45760  fourierdlem79  46170  fourierdlem96  46187  fourierdlem97  46188  fourierdlem98  46189  fourierdlem99  46190  fourierdlem105  46196  fourierdlem108  46199  fourierdlem110  46201  sge0val  46351  sge0z  46360  sge0revalmpt  46363  sge0sn  46364  sge0tsms  46365  sge0f1o  46367  sge0sup  46376  sge0resplit  46391  meaiuninclem  46465  smfsuplem2  46797  smfsup  46799  smfsupmpt  46800  smflimsuplem1  46805  smflimsuplem2  46806  smflimsuplem4  46808  smflimsuplem5  46809  smflimsuplem7  46811  smflimsup  46813