Theorem supeq1i 9392

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

Syntax hints:   = wceq 1541  supcsup 9385

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-in 3920  df-ss 3930  df-uni 4871  df-sup 9387

This theorem is referenced by:  supsn  9417  infrenegsup  12147  supxrmnf  13246  rpsup  13781  resup  13782  gcdcom  16404  gcdass  16439  ovolgelb  24881  itg2seq  25144  itg2i1fseq  25157  itg2cnlem1  25163  dvfsumrlim  25432  pserdvlem2  25824  logtayl  26052  nmopnegi  30970  nmop0  30991  nmfn0  30992  esumnul  32736  ismblfin  36192  ovoliunnfl  36193  voliunnfl  36195  itg2addnclem  36202  binomcxplemdvsum  42757  binomcxp  42759  supxrleubrnmptf  43806  limsup0  44055  limsupresico  44061  liminfresico  44132  liminf10ex  44135  ioodvbdlimc1lem1  44292  ioodvbdlimc1  44294  ioodvbdlimc2  44296  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  fourierdlem70  44537  fourierdlem71  44538  fourierdlem97  44564  fourierdlem103  44570  fourierdlem104  44571  fourierdlem109  44576  sge00  44737  sge0sn  44740  sge0xaddlem2  44795  decsmf  45128  smflimsuplem1  45181  smflimsuplem3  45183  smflimsup  45189