Theorem supeq1i 9443

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

This proof depends on syntax axioms:   = wceq 1569  supcsup 9436

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3896  df-uni 4867  df-sup 9438

This theorem is used by:  supsn  9469  infrenegsup  12304  supxrmnf  13451  rpsup  14010  resup  14011  gcdcom  16691  gcdass  16726  ovolgelb  25807  itg2seq  26069  itg2i1fseq  26082  itg2cnlem1  26088  dvfsumrlim  26357  pserdvlem2  26761  logtayl  26994  nmopnegi  32573  nmop0  32594  nmfn0  32595  esumnul  34727  ismblfin  38673  ovoliunnfl  38674  voliunnfl  38676  itg2addnclem  38683  binomcxplemdvsum  45433  binomcxp  45435  supxrleubrnmptf  46555  limsup0  46798  limsupresico  46804  liminfresico  46875  liminf10ex  46878  ioodvbdlimc1lem1  47035  ioodvbdlimc1  47037  ioodvbdlimc2  47039  fourierdlem41  47252  fourierdlem48  47258  fourierdlem49  47259  fourierdlem70  47280  fourierdlem71  47281  fourierdlem97  47307  fourierdlem103  47313  fourierdlem104  47314  fourierdlem109  47319  sge00  47480  sge0sn  47483  sge0xaddlem2  47538  decsmf  47871  smflimsuplem1  47924  smflimsuplem3  47926  smflimsup  47932