Theorem supeq1i 9487

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

Syntax hints:   = wceq 1540  supcsup 9480

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-ss 3968  df-uni 4908  df-sup 9482

This theorem is referenced by:  supsn  9512  infrenegsup  12251  supxrmnf  13359  rpsup  13906  resup  13907  gcdcom  16550  gcdass  16584  ovolgelb  25515  itg2seq  25777  itg2i1fseq  25790  itg2cnlem1  25796  dvfsumrlim  26072  pserdvlem2  26472  logtayl  26702  nmopnegi  31984  nmop0  32005  nmfn0  32006  esumnul  34049  ismblfin  37668  ovoliunnfl  37669  voliunnfl  37671  itg2addnclem  37678  binomcxplemdvsum  44374  binomcxp  44376  supxrleubrnmptf  45462  limsup0  45709  limsupresico  45715  liminfresico  45786  liminf10ex  45789  ioodvbdlimc1lem1  45946  ioodvbdlimc1  45948  ioodvbdlimc2  45950  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem70  46191  fourierdlem71  46192  fourierdlem97  46218  fourierdlem103  46224  fourierdlem104  46225  fourierdlem109  46230  sge00  46391  sge0sn  46394  sge0xaddlem2  46449  decsmf  46782  smflimsuplem1  46835  smflimsuplem3  46837  smflimsup  46843