Theorem supeq1i 9484

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

Syntax hints:   = wceq 1536  supcsup 9477

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-ss 3979  df-uni 4912  df-sup 9479

This theorem is referenced by:  supsn  9509  infrenegsup  12248  supxrmnf  13355  rpsup  13902  resup  13903  gcdcom  16546  gcdass  16580  ovolgelb  25528  itg2seq  25791  itg2i1fseq  25804  itg2cnlem1  25810  dvfsumrlim  26086  pserdvlem2  26486  logtayl  26716  nmopnegi  31993  nmop0  32014  nmfn0  32015  esumnul  34028  ismblfin  37647  ovoliunnfl  37648  voliunnfl  37650  itg2addnclem  37657  binomcxplemdvsum  44350  binomcxp  44352  supxrleubrnmptf  45400  limsup0  45649  limsupresico  45655  liminfresico  45726  liminf10ex  45729  ioodvbdlimc1lem1  45886  ioodvbdlimc1  45888  ioodvbdlimc2  45890  fourierdlem41  46103  fourierdlem48  46109  fourierdlem49  46110  fourierdlem70  46131  fourierdlem71  46132  fourierdlem97  46158  fourierdlem103  46164  fourierdlem104  46165  fourierdlem109  46170  sge00  46331  sge0sn  46334  sge0xaddlem2  46389  decsmf  46722  smflimsuplem1  46775  smflimsuplem3  46777  smflimsup  46783