Theorem supeq1i 9386

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

Syntax hints:   = wceq 1559  supcsup 9379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-ss 3919  df-uni 4863  df-sup 9381

This theorem is referenced by:  supsn  9412  infrenegsup  12168  supxrmnf  13313  rpsup  13869  resup  13870  gcdcom  16537  gcdass  16571  ovolgelb  25529  itg2seq  25791  itg2i1fseq  25804  itg2cnlem1  25810  dvfsumrlim  26080  pserdvlem2  26478  logtayl  26712  nmopnegi  32124  nmop0  32145  nmfn0  32146  esumnul  34305  ismblfin  38120  ovoliunnfl  38121  voliunnfl  38123  itg2addnclem  38130  binomcxplemdvsum  44891  binomcxp  44893  supxrleubrnmptf  45985  limsup0  46228  limsupresico  46234  liminfresico  46305  liminf10ex  46308  ioodvbdlimc1lem1  46465  ioodvbdlimc1  46467  ioodvbdlimc2  46469  fourierdlem41  46682  fourierdlem48  46688  fourierdlem49  46689  fourierdlem70  46710  fourierdlem71  46711  fourierdlem97  46737  fourierdlem103  46743  fourierdlem104  46744  fourierdlem109  46749  sge00  46910  sge0sn  46913  sge0xaddlem2  46968  decsmf  47301  smflimsuplem1  47354  smflimsuplem3  47356  smflimsup  47362