Theorem supeq1i 9417

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

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

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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3916  df-uni 4868  df-sup 9412

This theorem is used by:  supsn  9443  infrenegsup  12222  supxrmnf  13369  rpsup  13927  resup  13928  gcdcom  16603  gcdass  16637  ovolgelb  25708  itg2seq  25970  itg2i1fseq  25983  itg2cnlem1  25989  dvfsumrlim  26258  pserdvlem2  26664  logtayl  26897  nmopnegi  32446  nmop0  32467  nmfn0  32468  esumnul  34558  ismblfin  38410  ovoliunnfl  38411  voliunnfl  38413  itg2addnclem  38420  binomcxplemdvsum  45179  binomcxp  45181  supxrleubrnmptf  46279  limsup0  46522  limsupresico  46528  liminfresico  46599  liminf10ex  46602  ioodvbdlimc1lem1  46759  ioodvbdlimc1  46761  ioodvbdlimc2  46763  fourierdlem41  46976  fourierdlem48  46982  fourierdlem49  46983  fourierdlem70  47004  fourierdlem71  47005  fourierdlem97  47031  fourierdlem103  47037  fourierdlem104  47038  fourierdlem109  47043  sge00  47204  sge0sn  47207  sge0xaddlem2  47262  decsmf  47595  smflimsuplem1  47648  smflimsuplem3  47650  smflimsup  47656