Theorem supeq1d 9349

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

Syntax hints:   → wi 4   = wceq 1541  supcsup 9343

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-ss 3918  df-uni 4864  df-sup 9345

This theorem is referenced by:  supadd  12110  supminf  12848  rpnnen1lem6  12895  rpnnen1  12896  limsupval  15397  limsupgval  15399  gcdval  16423  gcdass  16474  pcval  16772  pceulem  16773  pceu  16774  pczpre  16775  pcdiv  16780  pcneg  16802  prmreclem1  16844  prmreclem5  16848  ramz  16953  prdsval  17375  prdsdsval  17398  prdsdsval2  17404  prdsdsval3  17405  ressprdsds  24315  xpsdsval  24325  tmsxpsval  24482  bndth  24913  elovolmr  25433  ovolctb  25447  ovoliunlem3  25461  ovolshftlem1  25466  voliunlem3  25509  voliun  25511  volsup  25513  ioorf  25530  mbfinf  25622  itg1climres  25671  itg2val  25685  itg2monolem1  25707  itg2i1fseq  25712  itg2cnlem1  25718  mdegfval  26023  mdegval  26024  mdeg0  26031  mdegvsca  26037  mdegpropd  26045  deg1val  26057  deg1mul3  26077  dgrval  26189  coe11  26214  nmoofval  30837  nmooval  30838  nmoo0  30866  nmopval  31931  nmfnval  31951  ressdeg1  33647  esumval  34203  esum0  34206  esumsnf  34221  esumfsupre  34228  esumsup  34246  erdszelem3  35387  erdsze  35396  elwlim  36015  ee7.2aOLD  36655  poimirlem32  37849  ovoliunnfl  37859  voliunnfl  37861  volsupnfl  37862  itg2addnc  37871  aomclem8  43299  infnsuprnmpt  45490  supsubc  45594  supxrmnf2  45673  supminfxr  45704  limsupval3  45932  limsupresre  45936  limsuplesup  45939  limsupresico  45940  limsupvaluz  45948  limsupvaluzmpt  45957  limsupvaluz2  45978  supcnvlimsup  45980  supcnvlimsupmpt  45981  limsuplt2  45993  liminfval  45999  limsupge  46001  liminfval5  46005  limsupresxr  46006  liminfresxr  46007  liminfresico  46011  limsup10ex  46013  liminflelimsuplem  46015  fourierdlem79  46425  fourierdlem96  46442  fourierdlem97  46443  fourierdlem98  46444  fourierdlem99  46445  fourierdlem105  46451  fourierdlem108  46454  fourierdlem110  46456  sge0val  46606  sge0z  46615  sge0revalmpt  46618  sge0sn  46619  sge0tsms  46620  sge0f1o  46622  sge0sup  46631  sge0resplit  46646  meaiuninclem  46720  smfsuplem2  47052  smfsup  47054  smfsupmpt  47055  smflimsuplem1  47060  smflimsuplem2  47061  smflimsuplem4  47063  smflimsuplem5  47064  smflimsuplem7  47066  smflimsup  47068