Theorem supeq1i 8353

Description: Equality inference for supremum. (Contributed by Paul Chapman, 22-Jun-2011.)

Hypothesis

Ref	Expression
supeq1i.1	|- B = C

Assertion

Ref	Expression
supeq1i	|- sup ( B , A , R ) = sup ( C , A , R )

Proof of Theorem supeq1i

Step	Hyp	Ref	Expression
1		supeq1i.1	. 2 |- B = C
2		supeq1 8351	. 2 |- ( B = C -> sup ( B , A , R ) = sup ( C , A , R ) )
3	1, 2	ax-mp 5	1 |- sup ( B , A , R ) = sup ( C , A , R )

Syntax hints:   = wceq 1483   supcsup 8346

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-uni 4437  df-sup 8348

This theorem is referenced by:  supsn  8378  infrenegsup  11006  supxrmnf  12147  rpsup  12665  resup  12666  gcdcom  15235  gcdass  15264  ovolgelb  23248  itg2seq  23509  itg2i1fseq  23522  itg2cnlem1  23528  dvfsumrlim  23794  pserdvlem2  24182  logtayl  24406  nmopnegi  28824  nmop0  28845  nmfn0  28846  esumnul  30110  ismblfin  33450  ovoliunnfl  33451  voliunnfl  33453  itg2addnclem  33461  binomcxplemdvsum  38554  binomcxp  38556  supxrleubrnmptf  39680  limsup0  39926  limsupresico  39932  liminfresico  40003  liminf10ex  40006  ioodvbdlimc1lem1  40146  ioodvbdlimc1  40148  ioodvbdlimc2  40150  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem70  40393  fourierdlem71  40394  fourierdlem97  40420  fourierdlem103  40426  fourierdlem104  40427  fourierdlem109  40432  sge00  40593  sge0sn  40596  sge0xaddlem2  40651  decsmf  40975  smflimsuplem1  41026  smflimsuplem3  41028  smflimsup  41034