Theorem supeq1i 9350

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

Syntax hints:   = wceq 1541  supcsup 9343

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-ss 3918  df-uni 4864  df-sup 9345

This theorem is referenced by:  supsn  9376  infrenegsup  12125  supxrmnf  13232  rpsup  13786  resup  13787  gcdcom  16440  gcdass  16474  ovolgelb  25437  itg2seq  25699  itg2i1fseq  25712  itg2cnlem1  25718  dvfsumrlim  25994  pserdvlem2  26394  logtayl  26625  nmopnegi  32040  nmop0  32061  nmfn0  32062  esumnul  34205  ismblfin  37862  ovoliunnfl  37863  voliunnfl  37865  itg2addnclem  37872  binomcxplemdvsum  44596  binomcxp  44598  supxrleubrnmptf  45695  limsup0  45938  limsupresico  45944  liminfresico  46015  liminf10ex  46018  ioodvbdlimc1lem1  46175  ioodvbdlimc1  46177  ioodvbdlimc2  46179  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem70  46420  fourierdlem71  46421  fourierdlem97  46447  fourierdlem103  46453  fourierdlem104  46454  fourierdlem109  46459  sge00  46620  sge0sn  46623  sge0xaddlem2  46678  decsmf  47011  smflimsuplem1  47064  smflimsuplem3  47066  smflimsup  47072