Theorem supeq1i 9444

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

Syntax hints:   = wceq 1539  supcsup 9437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-in 3954  df-ss 3964  df-uni 4908  df-sup 9439

This theorem is referenced by:  supsn  9469  infrenegsup  12201  supxrmnf  13300  rpsup  13835  resup  13836  gcdcom  16458  gcdass  16493  ovolgelb  25229  itg2seq  25492  itg2i1fseq  25505  itg2cnlem1  25511  dvfsumrlim  25783  pserdvlem2  26176  logtayl  26404  nmopnegi  31485  nmop0  31506  nmfn0  31507  esumnul  33344  ismblfin  36832  ovoliunnfl  36833  voliunnfl  36835  itg2addnclem  36842  binomcxplemdvsum  43416  binomcxp  43418  supxrleubrnmptf  44459  limsup0  44708  limsupresico  44714  liminfresico  44785  liminf10ex  44788  ioodvbdlimc1lem1  44945  ioodvbdlimc1  44947  ioodvbdlimc2  44949  fourierdlem41  45162  fourierdlem48  45168  fourierdlem49  45169  fourierdlem70  45190  fourierdlem71  45191  fourierdlem97  45217  fourierdlem103  45223  fourierdlem104  45224  fourierdlem109  45229  sge00  45390  sge0sn  45393  sge0xaddlem2  45448  decsmf  45781  smflimsuplem1  45834  smflimsuplem3  45836  smflimsup  45842