Theorem supeq1i 9340

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

Syntax hints:   = wceq 1541  supcsup 9333

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-ss 3915  df-uni 4861  df-sup 9335

This theorem is referenced by:  supsn  9366  infrenegsup  12114  supxrmnf  13220  rpsup  13774  resup  13775  gcdcom  16428  gcdass  16462  ovolgelb  25411  itg2seq  25673  itg2i1fseq  25686  itg2cnlem1  25692  dvfsumrlim  25968  pserdvlem2  26368  logtayl  26599  nmopnegi  31949  nmop0  31970  nmfn0  31971  esumnul  34084  ismblfin  37724  ovoliunnfl  37725  voliunnfl  37727  itg2addnclem  37734  binomcxplemdvsum  44475  binomcxp  44477  supxrleubrnmptf  45576  limsup0  45819  limsupresico  45825  liminfresico  45896  liminf10ex  45899  ioodvbdlimc1lem1  46056  ioodvbdlimc1  46058  ioodvbdlimc2  46060  fourierdlem41  46273  fourierdlem48  46279  fourierdlem49  46280  fourierdlem70  46301  fourierdlem71  46302  fourierdlem97  46328  fourierdlem103  46334  fourierdlem104  46335  fourierdlem109  46340  sge00  46501  sge0sn  46504  sge0xaddlem2  46559  decsmf  46892  smflimsuplem1  46945  smflimsuplem3  46947  smflimsup  46953