Theorem supeq1i 9459

Description: Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1i.1	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
supeq1i	⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)

Proof of Theorem supeq1i

Step	Hyp	Ref	Expression
1		supeq1i.1	. 2 ⊢ 𝐵 = 𝐶
2		supeq1 9457	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)

Syntax hints:   = wceq 1540  supcsup 9452

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-ss 3943  df-uni 4884  df-sup 9454

This theorem is referenced by:  supsn  9485  infrenegsup  12225  supxrmnf  13333  rpsup  13883  resup  13884  gcdcom  16532  gcdass  16566  ovolgelb  25433  itg2seq  25695  itg2i1fseq  25708  itg2cnlem1  25714  dvfsumrlim  25990  pserdvlem2  26390  logtayl  26621  nmopnegi  31946  nmop0  31967  nmfn0  31968  esumnul  34079  ismblfin  37685  ovoliunnfl  37686  voliunnfl  37688  itg2addnclem  37695  binomcxplemdvsum  44379  binomcxp  44381  supxrleubrnmptf  45478  limsup0  45723  limsupresico  45729  liminfresico  45800  liminf10ex  45803  ioodvbdlimc1lem1  45960  ioodvbdlimc1  45962  ioodvbdlimc2  45964  fourierdlem41  46177  fourierdlem48  46183  fourierdlem49  46184  fourierdlem70  46205  fourierdlem71  46206  fourierdlem97  46232  fourierdlem103  46238  fourierdlem104  46239  fourierdlem109  46244  sge00  46405  sge0sn  46408  sge0xaddlem2  46463  decsmf  46796  smflimsuplem1  46849  smflimsuplem3  46851  smflimsup  46857