Theorem supeq1d 8912

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

Syntax hints:   → wi 4   = wceq 1537  supcsup 8906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-in 3945  df-ss 3954  df-uni 4841  df-sup 8908

This theorem is referenced by:  supadd  11611  supminf  12338  rpnnen1lem6  12384  rpnnen1  12385  limsupval  14833  limsupgval  14835  gcdval  15847  gcdass  15897  pcval  16183  pceulem  16184  pceu  16185  pczpre  16186  pcdiv  16191  pcneg  16212  prmreclem1  16254  prmreclem5  16258  ramz  16363  prdsval  16730  prdsdsval  16753  prdsdsval2  16759  prdsdsval3  16760  ressprdsds  22983  xpsdsval  22993  tmsxpsval  23150  bndth  23564  elovolmr  24079  ovolctb  24093  ovoliunlem3  24107  ovolshftlem1  24112  voliunlem3  24155  voliun  24157  volsup  24159  ioorf  24176  mbfinf  24268  itg1climres  24317  itg2val  24331  itg2monolem1  24353  itg2i1fseq  24358  itg2cnlem1  24364  mdegfval  24658  mdegval  24659  mdeg0  24666  mdegvsca  24672  mdegpropd  24680  deg1val  24692  deg1mul3  24711  dgrval  24820  coe11  24845  nmoofval  28541  nmooval  28542  nmoo0  28570  nmopval  29635  nmfnval  29655  esumval  31307  esum0  31310  esumsnf  31325  esumfsupre  31332  esumsup  31350  erdszelem3  32442  erdsze  32451  elwlim  33112  ee7.2aOLD  33811  poimirlem32  34926  ovoliunnfl  34936  voliunnfl  34938  volsupnfl  34939  itg2addnc  34948  aomclem8  39668  infnsuprnmpt  41529  supsubc  41628  supxrmnf2  41714  supminfxr  41747  limsupval3  41980  limsupresre  41984  limsuplesup  41987  limsupresico  41988  limsupvaluz  41996  limsupvaluzmpt  42005  limsupvaluz2  42026  supcnvlimsup  42028  supcnvlimsupmpt  42029  limsuplt2  42041  liminfval  42047  limsupge  42049  liminfval5  42053  limsupresxr  42054  liminfresxr  42055  liminfresico  42059  limsup10ex  42061  liminflelimsuplem  42063  fourierdlem79  42477  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem105  42503  fourierdlem108  42506  fourierdlem110  42508  sge0val  42655  sge0z  42664  sge0revalmpt  42667  sge0sn  42668  sge0tsms  42669  sge0f1o  42671  sge0sup  42680  sge0resplit  42695  meaiuninclem  42769  smfsuplem2  43093  smfsup  43095  smfsupmpt  43096  smflimsuplem1  43101  smflimsuplem2  43102  smflimsuplem4  43104  smflimsuplem5  43105  smflimsuplem7  43107  smflimsup  43109