Theorem supeq1i 9356

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

Syntax hints:   = wceq 1540  supcsup 9349

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-ss 3922  df-uni 4862  df-sup 9351

This theorem is referenced by:  supsn  9382  infrenegsup  12126  supxrmnf  13237  rpsup  13788  resup  13789  gcdcom  16442  gcdass  16476  ovolgelb  25397  itg2seq  25659  itg2i1fseq  25672  itg2cnlem1  25678  dvfsumrlim  25954  pserdvlem2  26354  logtayl  26585  nmopnegi  31927  nmop0  31948  nmfn0  31949  esumnul  34017  ismblfin  37643  ovoliunnfl  37644  voliunnfl  37646  itg2addnclem  37653  binomcxplemdvsum  44331  binomcxp  44333  supxrleubrnmptf  45434  limsup0  45679  limsupresico  45685  liminfresico  45756  liminf10ex  45759  ioodvbdlimc1lem1  45916  ioodvbdlimc1  45918  ioodvbdlimc2  45920  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem70  46161  fourierdlem71  46162  fourierdlem97  46188  fourierdlem103  46194  fourierdlem104  46195  fourierdlem109  46200  sge00  46361  sge0sn  46364  sge0xaddlem2  46419  decsmf  46752  smflimsuplem1  46805  smflimsuplem3  46807  smflimsup  46813