Theorem supeq1i 9432

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-ss 3916  df-uni 4868  df-sup 9427

This theorem is used by:  supsn  9458  infrenegsup  12293  supxrmnf  13440  rpsup  13999  resup  14000  gcdcom  16678  gcdass  16713  ovolgelb  25794  itg2seq  26056  itg2i1fseq  26069  itg2cnlem1  26075  dvfsumrlim  26344  pserdvlem2  26748  logtayl  26981  nmopnegi  32560  nmop0  32581  nmfn0  32582  esumnul  34673  ismblfin  38559  ovoliunnfl  38560  voliunnfl  38562  itg2addnclem  38569  binomcxplemdvsum  45324  binomcxp  45326  supxrleubrnmptf  46430  limsup0  46673  limsupresico  46679  liminfresico  46750  liminf10ex  46753  ioodvbdlimc1lem1  46910  ioodvbdlimc1  46912  ioodvbdlimc2  46914  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  fourierdlem70  47155  fourierdlem71  47156  fourierdlem97  47182  fourierdlem103  47188  fourierdlem104  47189  fourierdlem109  47194  sge00  47355  sge0sn  47358  sge0xaddlem2  47413  decsmf  47746  smflimsuplem1  47799  smflimsuplem3  47801  smflimsup  47807