Theorem supeq1i 8469

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

Syntax hints:   = wceq 1596  supcsup 8462

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ral 3019  df-rex 3020  df-rab 3023  df-uni 4545  df-sup 8464

This theorem is referenced by:  supsn  8494  infrenegsup  11119  supxrmnf  12261  rpsup  12780  resup  12781  gcdcom  15358  gcdass  15387  ovolgelb  23369  itg2seq  23629  itg2i1fseq  23642  itg2cnlem1  23648  dvfsumrlim  23914  pserdvlem2  24302  logtayl  24526  nmopnegi  29054  nmop0  29075  nmfn0  29076  esumnul  30340  ismblfin  33682  ovoliunnfl  33683  voliunnfl  33685  itg2addnclem  33693  binomcxplemdvsum  38973  binomcxp  38975  supxrleubrnmptf  40095  limsup0  40346  limsupresico  40352  liminfresico  40423  liminf10ex  40426  ioodvbdlimc1lem1  40566  ioodvbdlimc1  40568  ioodvbdlimc2  40570  fourierdlem41  40785  fourierdlem48  40791  fourierdlem49  40792  fourierdlem70  40813  fourierdlem71  40814  fourierdlem97  40840  fourierdlem103  40846  fourierdlem104  40847  fourierdlem109  40852  sge00  41013  sge0sn  41016  sge0xaddlem2  41071  decsmf  41398  smflimsuplem1  41449  smflimsuplem3  41451  smflimsup  41457