Theorem supeq1i 9442

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

Syntax hints:   = wceq 1542  supcsup 9435

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-in 3956  df-ss 3966  df-uni 4910  df-sup 9437

This theorem is referenced by:  supsn  9467  infrenegsup  12197  supxrmnf  13296  rpsup  13831  resup  13832  gcdcom  16454  gcdass  16489  ovolgelb  24997  itg2seq  25260  itg2i1fseq  25273  itg2cnlem1  25279  dvfsumrlim  25548  pserdvlem2  25940  logtayl  26168  nmopnegi  31218  nmop0  31239  nmfn0  31240  esumnul  33046  ismblfin  36529  ovoliunnfl  36530  voliunnfl  36532  itg2addnclem  36539  binomcxplemdvsum  43114  binomcxp  43116  supxrleubrnmptf  44161  limsup0  44410  limsupresico  44416  liminfresico  44487  liminf10ex  44490  ioodvbdlimc1lem1  44647  ioodvbdlimc1  44649  ioodvbdlimc2  44651  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem70  44892  fourierdlem71  44893  fourierdlem97  44919  fourierdlem103  44925  fourierdlem104  44926  fourierdlem109  44931  sge00  45092  sge0sn  45095  sge0xaddlem2  45150  decsmf  45483  smflimsuplem1  45536  smflimsuplem3  45538  smflimsup  45544