Theorem supeq1i 9405

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

Syntax hints:   = wceq 1540  supcsup 9398

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-ss 3934  df-uni 4875  df-sup 9400

This theorem is referenced by:  supsn  9431  infrenegsup  12173  supxrmnf  13284  rpsup  13835  resup  13836  gcdcom  16490  gcdass  16524  ovolgelb  25388  itg2seq  25650  itg2i1fseq  25663  itg2cnlem1  25669  dvfsumrlim  25945  pserdvlem2  26345  logtayl  26576  nmopnegi  31901  nmop0  31922  nmfn0  31923  esumnul  34045  ismblfin  37662  ovoliunnfl  37663  voliunnfl  37665  itg2addnclem  37672  binomcxplemdvsum  44351  binomcxp  44353  supxrleubrnmptf  45454  limsup0  45699  limsupresico  45705  liminfresico  45776  liminf10ex  45779  ioodvbdlimc1lem1  45936  ioodvbdlimc1  45938  ioodvbdlimc2  45940  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  fourierdlem70  46181  fourierdlem71  46182  fourierdlem97  46208  fourierdlem103  46214  fourierdlem104  46215  fourierdlem109  46220  sge00  46381  sge0sn  46384  sge0xaddlem2  46439  decsmf  46772  smflimsuplem1  46825  smflimsuplem3  46827  smflimsup  46833