Theorem supeq1i 9331

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 9329	. 2 ⊢ (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
3	1, 2	ax-mp 5	1 ⊢ sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)

Syntax hints:   = wceq 1541  supcsup 9324

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-ss 3919  df-uni 4860  df-sup 9326

This theorem is referenced by:  supsn  9357  infrenegsup  12105  supxrmnf  13216  rpsup  13770  resup  13771  gcdcom  16424  gcdass  16458  ovolgelb  25409  itg2seq  25671  itg2i1fseq  25684  itg2cnlem1  25690  dvfsumrlim  25966  pserdvlem2  26366  logtayl  26597  nmopnegi  31943  nmop0  31964  nmfn0  31965  esumnul  34059  ismblfin  37707  ovoliunnfl  37708  voliunnfl  37710  itg2addnclem  37717  binomcxplemdvsum  44394  binomcxp  44396  supxrleubrnmptf  45495  limsup0  45738  limsupresico  45744  liminfresico  45815  liminf10ex  45818  ioodvbdlimc1lem1  45975  ioodvbdlimc1  45977  ioodvbdlimc2  45979  fourierdlem41  46192  fourierdlem48  46198  fourierdlem49  46199  fourierdlem70  46220  fourierdlem71  46221  fourierdlem97  46247  fourierdlem103  46253  fourierdlem104  46254  fourierdlem109  46259  sge00  46420  sge0sn  46423  sge0xaddlem2  46478  decsmf  46811  smflimsuplem1  46864  smflimsuplem3  46866  smflimsup  46872