Theorem supeq1i 9421

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

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ral 3079  df-rex 3089  df-rab 3415  df-v 3455  df-ss 3919  df-uni 4871  df-sup 9416

This theorem is used by:  supsn  9447  infrenegsup  12226  supxrmnf  13373  rpsup  13931  resup  13932  gcdcom  16609  gcdass  16643  ovolgelb  25714  itg2seq  25976  itg2i1fseq  25989  itg2cnlem1  25995  dvfsumrlim  26265  pserdvlem2  26671  logtayl  26905  nmopnegi  32454  nmop0  32475  nmfn0  32476  esumnul  34566  ismblfin  38418  ovoliunnfl  38419  voliunnfl  38421  itg2addnclem  38428  binomcxplemdvsum  45187  binomcxp  45189  supxrleubrnmptf  46287  limsup0  46530  limsupresico  46536  liminfresico  46607  liminf10ex  46610  ioodvbdlimc1lem1  46767  ioodvbdlimc1  46769  ioodvbdlimc2  46771  fourierdlem41  46984  fourierdlem48  46990  fourierdlem49  46991  fourierdlem70  47012  fourierdlem71  47013  fourierdlem97  47039  fourierdlem103  47045  fourierdlem104  47046  fourierdlem109  47051  sge00  47212  sge0sn  47215  sge0xaddlem2  47270  decsmf  47603  smflimsuplem1  47656  smflimsuplem3  47658  smflimsup  47664