Theorem supeq1i 9136

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

Syntax hints:   = wceq 1539  supcsup 9129

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-in 3890  df-ss 3900  df-uni 4837  df-sup 9131

This theorem is referenced by:  supsn  9161  infrenegsup  11888  supxrmnf  12980  rpsup  13514  resup  13515  gcdcom  16148  gcdass  16183  ovolgelb  24549  itg2seq  24812  itg2i1fseq  24825  itg2cnlem1  24831  dvfsumrlim  25100  pserdvlem2  25492  logtayl  25720  nmopnegi  30228  nmop0  30249  nmfn0  30250  esumnul  31916  ismblfin  35745  ovoliunnfl  35746  voliunnfl  35748  itg2addnclem  35755  binomcxplemdvsum  41862  binomcxp  41864  supxrleubrnmptf  42881  limsup0  43125  limsupresico  43131  liminfresico  43202  liminf10ex  43205  ioodvbdlimc1lem1  43362  ioodvbdlimc1  43364  ioodvbdlimc2  43366  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  fourierdlem70  43607  fourierdlem71  43608  fourierdlem97  43634  fourierdlem103  43640  fourierdlem104  43641  fourierdlem109  43646  sge00  43804  sge0sn  43807  sge0xaddlem2  43862  decsmf  44189  smflimsuplem1  44240  smflimsuplem3  44242  smflimsup  44248