Theorem supeq1i 9362

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

Syntax hints:   = wceq 1542  supcsup 9355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-ss 3920  df-uni 4866  df-sup 9357

This theorem is referenced by:  supsn  9388  infrenegsup  12137  supxrmnf  13244  rpsup  13798  resup  13799  gcdcom  16452  gcdass  16486  ovolgelb  25449  itg2seq  25711  itg2i1fseq  25724  itg2cnlem1  25730  dvfsumrlim  26006  pserdvlem2  26406  logtayl  26637  nmopnegi  32052  nmop0  32073  nmfn0  32074  esumnul  34225  ismblfin  37909  ovoliunnfl  37910  voliunnfl  37912  itg2addnclem  37919  binomcxplemdvsum  44708  binomcxp  44710  supxrleubrnmptf  45806  limsup0  46049  limsupresico  46055  liminfresico  46126  liminf10ex  46129  ioodvbdlimc1lem1  46286  ioodvbdlimc1  46288  ioodvbdlimc2  46290  fourierdlem41  46503  fourierdlem48  46509  fourierdlem49  46510  fourierdlem70  46531  fourierdlem71  46532  fourierdlem97  46558  fourierdlem103  46564  fourierdlem104  46565  fourierdlem109  46570  sge00  46731  sge0sn  46734  sge0xaddlem2  46789  decsmf  47122  smflimsuplem1  47175  smflimsuplem3  47177  smflimsup  47183