Theorem supeq1i 9354

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

Syntax hints:   = wceq 1542  supcsup 9347

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3062  df-rab 3401  df-v 3443  df-ss 3919  df-uni 4865  df-sup 9349

This theorem is referenced by:  supsn  9380  infrenegsup  12129  supxrmnf  13236  rpsup  13790  resup  13791  gcdcom  16444  gcdass  16478  ovolgelb  25441  itg2seq  25703  itg2i1fseq  25716  itg2cnlem1  25722  dvfsumrlim  25998  pserdvlem2  26398  logtayl  26629  nmopnegi  32023  nmop0  32044  nmfn0  32045  esumnul  34186  ismblfin  37833  ovoliunnfl  37834  voliunnfl  37836  itg2addnclem  37843  binomcxplemdvsum  44632  binomcxp  44634  supxrleubrnmptf  45731  limsup0  45974  limsupresico  45980  liminfresico  46051  liminf10ex  46054  ioodvbdlimc1lem1  46211  ioodvbdlimc1  46213  ioodvbdlimc2  46215  fourierdlem41  46428  fourierdlem48  46434  fourierdlem49  46435  fourierdlem70  46456  fourierdlem71  46457  fourierdlem97  46483  fourierdlem103  46489  fourierdlem104  46490  fourierdlem109  46495  sge00  46656  sge0sn  46659  sge0xaddlem2  46714  decsmf  47047  smflimsuplem1  47100  smflimsuplem3  47102  smflimsup  47108