Theorem supeq1d 9422

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  supcsup 9416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-ss 3916  df-uni 4868  df-sup 9418

This theorem is used by:  supadd  12266  supminf  13043  rpnnen1lem6  13091  rpnnen1  13092  limsupval  15621  limsupgval  15623  gcdval  16646  gcdass  16700  pcval  17002  pceulem  17003  pceu  17004  pczpre  17005  pcdiv  17010  pcneg  17032  prmreclem1  17074  prmreclem5  17078  ramz  17183  prdsval  17606  prdsdsval  17629  prdsdsval2  17635  prdsdsval3  17636  ressprdsds  24670  xpsdsval  24680  tmsxpsval  24837  bndth  25259  elovolmr  25777  ovolctb  25791  ovoliunlem3  25805  ovolshftlem1  25810  voliunlem3  25853  voliun  25855  volsup  25857  ioorf  25874  mbfinf  25966  itg1climres  26015  itg2val  26029  itg2monolem1  26051  itg2i1fseq  26056  itg2cnlem1  26062  mdegfval  26360  mdegval  26361  mdeg0  26368  mdegvsca  26374  mdegpropd  26382  deg1val  26394  deg1mul3  26414  dgrval  26527  coe11  26552  nmoofval  31346  nmooval  31347  nmoo0  31375  nmopval  32440  nmfnval  32460  ressdeg1  34080  esumval  34660  esum0  34663  esumsnf  34678  esumfsupre  34685  esumsup  34703  erdszelem3  35927  erdsze  35936  elwlim  36555  ee7.2aOLD  37219  poimirlem32  38538  ovoliunnfl  38548  voliunnfl  38550  volsupnfl  38551  itg2addnc  38560  aomclem8  44021  infnsuprnmpt  46205  supsubc  46309  supxrmnf2  46387  supminfxr  46418  limsupval3  46646  limsupresre  46650  limsuplesup  46653  limsupresico  46654  limsupvaluz  46662  limsupvaluzmpt  46671  limsupvaluz2  46692  supcnvlimsup  46694  supcnvlimsupmpt  46695  limsuplt2  46707  liminfval  46713  limsupge  46715  liminfval5  46719  limsupresxr  46720  liminfresxr  46721  liminfresico  46725  limsup10ex  46727  liminflelimsuplem  46729  fourierdlem79  47139  fourierdlem96  47156  fourierdlem97  47157  fourierdlem98  47158  fourierdlem99  47159  fourierdlem105  47165  fourierdlem108  47168  fourierdlem110  47170  sge0val  47320  sge0z  47329  sge0revalmpt  47332  sge0sn  47333  sge0tsms  47334  sge0f1o  47336  sge0sup  47345  sge0resplit  47360  meaiuninclem  47434  smfsuplem2  47766  smfsup  47768  smfsupmpt  47769  smflimsuplem1  47774  smflimsuplem2  47775  smflimsuplem4  47777  smflimsuplem5  47778  smflimsuplem7  47780  smflimsup  47782