Theorem supeq1d 9437

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

Syntax hints:   → wi 4   = wceq 1541  supcsup 9431

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-in 3954  df-ss 3964  df-uni 4908  df-sup 9433

This theorem is referenced by:  supadd  12178  supminf  12915  rpnnen1lem6  12962  rpnnen1  12963  limsupval  15414  limsupgval  15416  gcdval  16433  gcdass  16485  pcval  16773  pceulem  16774  pceu  16775  pczpre  16776  pcdiv  16781  pcneg  16803  prmreclem1  16845  prmreclem5  16849  ramz  16954  prdsval  17397  prdsdsval  17420  prdsdsval2  17426  prdsdsval3  17427  ressprdsds  23868  xpsdsval  23878  tmsxpsval  24038  bndth  24465  elovolmr  24984  ovolctb  24998  ovoliunlem3  25012  ovolshftlem1  25017  voliunlem3  25060  voliun  25062  volsup  25064  ioorf  25081  mbfinf  25173  itg1climres  25223  itg2val  25237  itg2monolem1  25259  itg2i1fseq  25264  itg2cnlem1  25270  mdegfval  25571  mdegval  25572  mdeg0  25579  mdegvsca  25585  mdegpropd  25593  deg1val  25605  deg1mul3  25624  dgrval  25733  coe11  25758  nmoofval  30002  nmooval  30003  nmoo0  30031  nmopval  31096  nmfnval  31116  ressdeg1  32639  esumval  33032  esum0  33035  esumsnf  33050  esumfsupre  33057  esumsup  33075  erdszelem3  34172  erdsze  34181  elwlim  34783  ee7.2aOLD  35334  poimirlem32  36508  ovoliunnfl  36518  voliunnfl  36520  volsupnfl  36521  itg2addnc  36530  aomclem8  41788  infnsuprnmpt  43940  supsubc  44049  supxrmnf2  44129  supminfxr  44160  limsupval3  44394  limsupresre  44398  limsuplesup  44401  limsupresico  44402  limsupvaluz  44410  limsupvaluzmpt  44419  limsupvaluz2  44440  supcnvlimsup  44442  supcnvlimsupmpt  44443  limsuplt2  44455  liminfval  44461  limsupge  44463  liminfval5  44467  limsupresxr  44468  liminfresxr  44469  liminfresico  44473  limsup10ex  44475  liminflelimsuplem  44477  fourierdlem79  44887  fourierdlem96  44904  fourierdlem97  44905  fourierdlem98  44906  fourierdlem99  44907  fourierdlem105  44913  fourierdlem108  44916  fourierdlem110  44918  sge0val  45068  sge0z  45077  sge0revalmpt  45080  sge0sn  45081  sge0tsms  45082  sge0f1o  45084  sge0sup  45093  sge0resplit  45108  meaiuninclem  45182  smfsuplem2  45514  smfsup  45516  smfsupmpt  45517  smflimsuplem1  45522  smflimsuplem2  45523  smflimsuplem4  45525  smflimsuplem5  45526  smflimsuplem7  45528  smflimsup  45530