Theorem supeq1i 9516

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

Syntax hints:   = wceq 1537  supcsup 9509

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-ss 3993  df-uni 4932  df-sup 9511

This theorem is referenced by:  supsn  9541  infrenegsup  12278  supxrmnf  13379  rpsup  13917  resup  13918  gcdcom  16559  gcdass  16594  ovolgelb  25534  itg2seq  25797  itg2i1fseq  25810  itg2cnlem1  25816  dvfsumrlim  26092  pserdvlem2  26490  logtayl  26720  nmopnegi  31997  nmop0  32018  nmfn0  32019  esumnul  34012  ismblfin  37621  ovoliunnfl  37622  voliunnfl  37624  itg2addnclem  37631  binomcxplemdvsum  44324  binomcxp  44326  supxrleubrnmptf  45366  limsup0  45615  limsupresico  45621  liminfresico  45692  liminf10ex  45695  ioodvbdlimc1lem1  45852  ioodvbdlimc1  45854  ioodvbdlimc2  45856  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem70  46097  fourierdlem71  46098  fourierdlem97  46124  fourierdlem103  46130  fourierdlem104  46131  fourierdlem109  46136  sge00  46297  sge0sn  46300  sge0xaddlem2  46355  decsmf  46688  smflimsuplem1  46741  smflimsuplem3  46743  smflimsup  46749