Theorem supeq1i 9476

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

This proof depends on syntax axioms:   = wceq 1570  supcsup 9469

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-uni 4873  df-sup 9471

This theorem is used by:  supsn  9502  infrenegsup  12340  supxrmnf  13487  rpsup  14046  resup  14047  gcdcom  16729  gcdass  16764  ovolgelb  25856  itg2seq  26118  itg2i1fseq  26131  itg2cnlem1  26137  dvfsumrlim  26406  pserdvlem2  26812  logtayl  27045  nmopnegi  32624  nmop0  32645  nmfn0  32646  esumnul  34791  ismblfin  38847  ovoliunnfl  38848  voliunnfl  38850  itg2addnclem  38857  binomcxplemdvsum  45600  binomcxp  45602  supxrleubrnmptf  46734  limsup0  46977  limsupresico  46983  liminfresico  47054  liminf10ex  47057  ioodvbdlimc1lem1  47214  ioodvbdlimc1  47216  ioodvbdlimc2  47218  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  fourierdlem70  47459  fourierdlem71  47460  fourierdlem97  47486  fourierdlem103  47492  fourierdlem104  47493  fourierdlem109  47498  sge00  47659  sge0sn  47662  sge0xaddlem2  47717  decsmf  48050  smflimsuplem1  48103  smflimsuplem3  48105  smflimsup  48111