Theorem supeq1i 9360

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

Syntax hints:   = wceq 1542  supcsup 9353

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-ss 3906  df-uni 4851  df-sup 9355

This theorem is referenced by:  supsn  9386  infrenegsup  12139  supxrmnf  13269  rpsup  13825  resup  13826  gcdcom  16482  gcdass  16516  ovolgelb  25447  itg2seq  25709  itg2i1fseq  25722  itg2cnlem1  25728  dvfsumrlim  25998  pserdvlem2  26393  logtayl  26624  nmopnegi  32036  nmop0  32057  nmfn0  32058  esumnul  34192  ismblfin  37982  ovoliunnfl  37983  voliunnfl  37985  itg2addnclem  37992  binomcxplemdvsum  44782  binomcxp  44784  supxrleubrnmptf  45879  limsup0  46122  limsupresico  46128  liminfresico  46199  liminf10ex  46202  ioodvbdlimc1lem1  46359  ioodvbdlimc1  46361  ioodvbdlimc2  46363  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  fourierdlem70  46604  fourierdlem71  46605  fourierdlem97  46631  fourierdlem103  46637  fourierdlem104  46638  fourierdlem109  46643  sge00  46804  sge0sn  46807  sge0xaddlem2  46862  decsmf  47195  smflimsuplem1  47248  smflimsuplem3  47250  smflimsup  47256