Theorem supeq1i 8905

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

Syntax hints:   = wceq 1533  supcsup 8898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-ral 3143  df-rex 3144  df-rab 3147  df-uni 4832  df-sup 8900

This theorem is referenced by:  supsn  8930  infrenegsup  11618  supxrmnf  12704  rpsup  13228  resup  13229  gcdcom  15856  gcdass  15889  ovolgelb  24075  itg2seq  24337  itg2i1fseq  24350  itg2cnlem1  24356  dvfsumrlim  24622  pserdvlem2  25010  logtayl  25237  nmopnegi  29736  nmop0  29757  nmfn0  29758  esumnul  31302  ismblfin  34927  ovoliunnfl  34928  voliunnfl  34930  itg2addnclem  34937  binomcxplemdvsum  40680  binomcxp  40682  supxrleubrnmptf  41720  limsup0  41968  limsupresico  41974  liminfresico  42045  liminf10ex  42048  ioodvbdlimc1lem1  42209  ioodvbdlimc1  42211  ioodvbdlimc2  42213  fourierdlem41  42427  fourierdlem48  42433  fourierdlem49  42434  fourierdlem70  42455  fourierdlem71  42456  fourierdlem97  42482  fourierdlem103  42488  fourierdlem104  42489  fourierdlem109  42494  sge00  42652  sge0sn  42655  sge0xaddlem2  42710  decsmf  43037  smflimsuplem1  43088  smflimsuplem3  43090  smflimsup  43096