Theorem supeq1i 9410

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

This proof depends on syntax axioms:   = wceq 1570  supcsup 9403

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-ss 3923  df-uni 4875  df-sup 9405

This theorem is used by:  supsn  9436  infrenegsup  12209  supxrmnf  13354  rpsup  13912  resup  13913  gcdcom  16588  gcdass  16622  ovolgelb  25668  itg2seq  25930  itg2i1fseq  25943  itg2cnlem1  25949  dvfsumrlim  26219  pserdvlem2  26620  logtayl  26854  nmopnegi  32346  nmop0  32367  nmfn0  32368  esumnul  34461  ismblfin  38345  ovoliunnfl  38346  voliunnfl  38348  itg2addnclem  38355  binomcxplemdvsum  45098  binomcxp  45100  supxrleubrnmptf  46198  limsup0  46441  limsupresico  46447  liminfresico  46518  liminf10ex  46521  ioodvbdlimc1lem1  46678  ioodvbdlimc1  46680  ioodvbdlimc2  46682  fourierdlem41  46895  fourierdlem48  46901  fourierdlem49  46902  fourierdlem70  46923  fourierdlem71  46924  fourierdlem97  46950  fourierdlem103  46956  fourierdlem104  46957  fourierdlem109  46962  sge00  47123  sge0sn  47126  sge0xaddlem2  47181  decsmf  47514  smflimsuplem1  47567  smflimsuplem3  47569  smflimsup  47575