Theorem supeq1d 9062

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

Syntax hints:   → wi 4   = wceq 1543  supcsup 9056

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-in 3873  df-ss 3883  df-uni 4820  df-sup 9058

This theorem is referenced by:  supadd  11800  supminf  12531  rpnnen1lem6  12578  rpnnen1  12579  limsupval  15035  limsupgval  15037  gcdval  16055  gcdass  16107  pcval  16397  pceulem  16398  pceu  16399  pczpre  16400  pcdiv  16405  pcneg  16427  prmreclem1  16469  prmreclem5  16473  ramz  16578  prdsval  16960  prdsdsval  16983  prdsdsval2  16989  prdsdsval3  16990  ressprdsds  23269  xpsdsval  23279  tmsxpsval  23436  bndth  23855  elovolmr  24373  ovolctb  24387  ovoliunlem3  24401  ovolshftlem1  24406  voliunlem3  24449  voliun  24451  volsup  24453  ioorf  24470  mbfinf  24562  itg1climres  24612  itg2val  24626  itg2monolem1  24648  itg2i1fseq  24653  itg2cnlem1  24659  mdegfval  24960  mdegval  24961  mdeg0  24968  mdegvsca  24974  mdegpropd  24982  deg1val  24994  deg1mul3  25013  dgrval  25122  coe11  25147  nmoofval  28843  nmooval  28844  nmoo0  28872  nmopval  29937  nmfnval  29957  esumval  31726  esum0  31729  esumsnf  31744  esumfsupre  31751  esumsup  31769  erdszelem3  32868  erdsze  32877  elwlim  33554  ee7.2aOLD  34387  poimirlem32  35546  ovoliunnfl  35556  voliunnfl  35558  volsupnfl  35559  itg2addnc  35568  aomclem8  40589  infnsuprnmpt  42468  supsubc  42565  supxrmnf2  42646  supminfxr  42679  limsupval3  42908  limsupresre  42912  limsuplesup  42915  limsupresico  42916  limsupvaluz  42924  limsupvaluzmpt  42933  limsupvaluz2  42954  supcnvlimsup  42956  supcnvlimsupmpt  42957  limsuplt2  42969  liminfval  42975  limsupge  42977  liminfval5  42981  limsupresxr  42982  liminfresxr  42983  liminfresico  42987  limsup10ex  42989  liminflelimsuplem  42991  fourierdlem79  43401  fourierdlem96  43418  fourierdlem97  43419  fourierdlem98  43420  fourierdlem99  43421  fourierdlem105  43427  fourierdlem108  43430  fourierdlem110  43432  sge0val  43579  sge0z  43588  sge0revalmpt  43591  sge0sn  43592  sge0tsms  43593  sge0f1o  43595  sge0sup  43604  sge0resplit  43619  meaiuninclem  43693  smfsuplem2  44017  smfsup  44019  smfsupmpt  44020  smflimsuplem1  44025  smflimsuplem2  44026  smflimsuplem4  44028  smflimsuplem5  44029  smflimsuplem7  44031  smflimsup  44033