Theorem supeq1i 9206

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

Syntax hints:   = wceq 1539  supcsup 9199

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-in 3894  df-ss 3904  df-uni 4840  df-sup 9201

This theorem is referenced by:  supsn  9231  infrenegsup  11958  supxrmnf  13051  rpsup  13586  resup  13587  gcdcom  16220  gcdass  16255  ovolgelb  24644  itg2seq  24907  itg2i1fseq  24920  itg2cnlem1  24926  dvfsumrlim  25195  pserdvlem2  25587  logtayl  25815  nmopnegi  30327  nmop0  30348  nmfn0  30349  esumnul  32016  ismblfin  35818  ovoliunnfl  35819  voliunnfl  35821  itg2addnclem  35828  binomcxplemdvsum  41973  binomcxp  41975  supxrleubrnmptf  42991  limsup0  43235  limsupresico  43241  liminfresico  43312  liminf10ex  43315  ioodvbdlimc1lem1  43472  ioodvbdlimc1  43474  ioodvbdlimc2  43476  fourierdlem41  43689  fourierdlem48  43695  fourierdlem49  43696  fourierdlem70  43717  fourierdlem71  43718  fourierdlem97  43744  fourierdlem103  43750  fourierdlem104  43751  fourierdlem109  43756  sge00  43914  sge0sn  43917  sge0xaddlem2  43972  decsmf  44302  smflimsuplem1  44353  smflimsuplem3  44355  smflimsup  44361