Theorem supeq1i 9408

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

Syntax hints:   = wceq 1570  supcsup 9401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-ss 3923  df-uni 4874  df-sup 9403

This theorem is referenced by:  supsn  9434  infrenegsup  12199  supxrmnf  13344  rpsup  13901  resup  13902  gcdcom  16572  gcdass  16606  ovolgelb  25620  itg2seq  25882  itg2i1fseq  25895  itg2cnlem1  25901  dvfsumrlim  26171  pserdvlem2  26572  logtayl  26806  nmopnegi  32298  nmop0  32319  nmfn0  32320  esumnul  34419  ismblfin  38293  ovoliunnfl  38294  voliunnfl  38296  itg2addnclem  38303  binomcxplemdvsum  45048  binomcxp  45050  supxrleubrnmptf  46148  limsup0  46391  limsupresico  46397  liminfresico  46468  liminf10ex  46471  ioodvbdlimc1lem1  46628  ioodvbdlimc1  46630  ioodvbdlimc2  46632  fourierdlem41  46845  fourierdlem48  46851  fourierdlem49  46852  fourierdlem70  46873  fourierdlem71  46874  fourierdlem97  46900  fourierdlem103  46906  fourierdlem104  46907  fourierdlem109  46912  sge00  47073  sge0sn  47076  sge0xaddlem2  47131  decsmf  47464  smflimsuplem1  47517  smflimsuplem3  47519  smflimsup  47525