Theorem supeq1i 9438

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

Syntax hints:   = wceq 1542  supcsup 9431

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 3954  df-ss 3964  df-uni 4908  df-sup 9433

This theorem is referenced by:  supsn  9463  infrenegsup  12193  supxrmnf  13292  rpsup  13827  resup  13828  gcdcom  16450  gcdass  16485  ovolgelb  24979  itg2seq  25242  itg2i1fseq  25255  itg2cnlem1  25261  dvfsumrlim  25530  pserdvlem2  25922  logtayl  26150  nmopnegi  31196  nmop0  31217  nmfn0  31218  esumnul  32984  ismblfin  36467  ovoliunnfl  36468  voliunnfl  36470  itg2addnclem  36477  binomcxplemdvsum  43047  binomcxp  43049  supxrleubrnmptf  44096  limsup0  44345  limsupresico  44351  liminfresico  44422  liminf10ex  44425  ioodvbdlimc1lem1  44582  ioodvbdlimc1  44584  ioodvbdlimc2  44586  fourierdlem41  44799  fourierdlem48  44805  fourierdlem49  44806  fourierdlem70  44827  fourierdlem71  44828  fourierdlem97  44854  fourierdlem103  44860  fourierdlem104  44861  fourierdlem109  44866  sge00  45027  sge0sn  45030  sge0xaddlem2  45085  decsmf  45418  smflimsuplem1  45471  smflimsuplem3  45473  smflimsup  45479