Theorem supeq1i 9395

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

Syntax hints:   = wceq 1563  supcsup 9388

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ral 3080  df-rex 3090  df-rab 3418  df-v 3459  df-ss 3924  df-uni 4868  df-sup 9390

This theorem is referenced by:  supsn  9421  infrenegsup  12186  supxrmnf  13331  rpsup  13887  resup  13888  gcdcom  16559  gcdass  16593  ovolgelb  25596  itg2seq  25858  itg2i1fseq  25871  itg2cnlem1  25877  dvfsumrlim  26147  pserdvlem2  26545  logtayl  26779  nmopnegi  32222  nmop0  32243  nmfn0  32244  esumnul  34350  ismblfin  38167  ovoliunnfl  38168  voliunnfl  38170  itg2addnclem  38177  binomcxplemdvsum  44924  binomcxp  44926  supxrleubrnmptf  46024  limsup0  46267  limsupresico  46273  liminfresico  46344  liminf10ex  46347  ioodvbdlimc1lem1  46504  ioodvbdlimc1  46506  ioodvbdlimc2  46508  fourierdlem41  46721  fourierdlem48  46727  fourierdlem49  46728  fourierdlem70  46749  fourierdlem71  46750  fourierdlem97  46776  fourierdlem103  46782  fourierdlem104  46783  fourierdlem109  46788  sge00  46949  sge0sn  46952  sge0xaddlem2  47007  decsmf  47340  smflimsuplem1  47393  smflimsuplem3  47395  smflimsup  47401