Theorem supeq1i 9398

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

Syntax hints:   = wceq 1540  supcsup 9391

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-ss 3931  df-uni 4872  df-sup 9393

This theorem is referenced by:  supsn  9424  infrenegsup  12166  supxrmnf  13277  rpsup  13828  resup  13829  gcdcom  16483  gcdass  16517  ovolgelb  25381  itg2seq  25643  itg2i1fseq  25656  itg2cnlem1  25662  dvfsumrlim  25938  pserdvlem2  26338  logtayl  26569  nmopnegi  31894  nmop0  31915  nmfn0  31916  esumnul  34038  ismblfin  37655  ovoliunnfl  37656  voliunnfl  37658  itg2addnclem  37665  binomcxplemdvsum  44344  binomcxp  44346  supxrleubrnmptf  45447  limsup0  45692  limsupresico  45698  liminfresico  45769  liminf10ex  45772  ioodvbdlimc1lem1  45929  ioodvbdlimc1  45931  ioodvbdlimc2  45933  fourierdlem41  46146  fourierdlem48  46152  fourierdlem49  46153  fourierdlem70  46174  fourierdlem71  46175  fourierdlem97  46201  fourierdlem103  46207  fourierdlem104  46208  fourierdlem109  46213  sge00  46374  sge0sn  46377  sge0xaddlem2  46432  decsmf  46765  smflimsuplem1  46818  smflimsuplem3  46820  smflimsup  46826