Theorem supeq1i 9353

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

Syntax hints:   = wceq 1542  supcsup 9346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-ss 3907  df-uni 4852  df-sup 9348

This theorem is referenced by:  supsn  9379  infrenegsup  12130  supxrmnf  13260  rpsup  13816  resup  13817  gcdcom  16473  gcdass  16507  ovolgelb  25457  itg2seq  25719  itg2i1fseq  25732  itg2cnlem1  25738  dvfsumrlim  26008  pserdvlem2  26406  logtayl  26637  nmopnegi  32051  nmop0  32072  nmfn0  32073  esumnul  34208  ismblfin  37996  ovoliunnfl  37997  voliunnfl  37999  itg2addnclem  38006  binomcxplemdvsum  44800  binomcxp  44802  supxrleubrnmptf  45897  limsup0  46140  limsupresico  46146  liminfresico  46217  liminf10ex  46220  ioodvbdlimc1lem1  46377  ioodvbdlimc1  46379  ioodvbdlimc2  46381  fourierdlem41  46594  fourierdlem48  46600  fourierdlem49  46601  fourierdlem70  46622  fourierdlem71  46623  fourierdlem97  46649  fourierdlem103  46655  fourierdlem104  46656  fourierdlem109  46661  sge00  46822  sge0sn  46825  sge0xaddlem2  46880  decsmf  47213  smflimsuplem1  47266  smflimsuplem3  47268  smflimsup  47274