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  37853  ovoliunnfl  37863  voliunnfl  37865  volsupnfl  37866  itg2addnc  37875  aomclem8  43303  infnsuprnmpt  45494  supsubc  45598  supxrmnf2  45677  supminfxr  45708  limsupval3  45936  limsupresre  45940  limsuplesup  45943  limsupresico  45944  limsupvaluz  45952  limsupvaluzmpt  45961  limsupvaluz2  45982  supcnvlimsup  45984  supcnvlimsupmpt  45985  limsuplt2  45997  liminfval  46003  limsupge  46005  liminfval5  46009  limsupresxr  46010  liminfresxr  46011  liminfresico  46015  limsup10ex  46017  liminflelimsuplem  46019  fourierdlem79  46429  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem105  46455  fourierdlem108  46458  fourierdlem110  46460  sge0val  46610  sge0z  46619  sge0revalmpt  46622  sge0sn  46623  sge0tsms  46624  sge0f1o  46626  sge0sup  46635  sge0resplit  46650  meaiuninclem  46724  smfsuplem2  47056  smfsup  47058  smfsupmpt  47059  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem4  47067  smflimsuplem5  47068  smflimsuplem7  47070  smflimsup  47072