Theorem supeq1i 8895

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

Syntax hints:   = wceq 1538  supcsup 8888

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-in 3888  df-ss 3898  df-uni 4801  df-sup 8890

This theorem is referenced by:  supsn  8920  infrenegsup  11611  supxrmnf  12698  rpsup  13229  resup  13230  gcdcom  15852  gcdass  15885  ovolgelb  24084  itg2seq  24346  itg2i1fseq  24359  itg2cnlem1  24365  dvfsumrlim  24634  pserdvlem2  25023  logtayl  25251  nmopnegi  29748  nmop0  29769  nmfn0  29770  esumnul  31417  ismblfin  35098  ovoliunnfl  35099  voliunnfl  35101  itg2addnclem  35108  binomcxplemdvsum  41059  binomcxp  41061  supxrleubrnmptf  42090  limsup0  42336  limsupresico  42342  liminfresico  42413  liminf10ex  42416  ioodvbdlimc1lem1  42573  ioodvbdlimc1  42575  ioodvbdlimc2  42577  fourierdlem41  42790  fourierdlem48  42796  fourierdlem49  42797  fourierdlem70  42818  fourierdlem71  42819  fourierdlem97  42845  fourierdlem103  42851  fourierdlem104  42852  fourierdlem109  42857  sge00  43015  sge0sn  43018  sge0xaddlem2  43073  decsmf  43400  smflimsuplem1  43451  smflimsuplem3  43453  smflimsup  43459