Theorem supeq1i 9357

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

Syntax hints:   = wceq 1547  supcsup 9350

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-ss 3907  df-uni 4846  df-sup 9352

This theorem is referenced by:  supsn  9383  infrenegsup  12137  supxrmnf  13267  rpsup  13823  resup  13824  gcdcom  16480  gcdass  16514  ovolgelb  25472  itg2seq  25734  itg2i1fseq  25747  itg2cnlem1  25753  dvfsumrlim  26023  pserdvlem2  26418  logtayl  26649  nmopnegi  32061  nmop0  32082  nmfn0  32083  esumnul  34239  ismblfin  38035  ovoliunnfl  38036  voliunnfl  38038  itg2addnclem  38045  binomcxplemdvsum  44806  binomcxp  44808  supxrleubrnmptf  45901  limsup0  46144  limsupresico  46150  liminfresico  46221  liminf10ex  46224  ioodvbdlimc1lem1  46381  ioodvbdlimc1  46383  ioodvbdlimc2  46385  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem70  46626  fourierdlem71  46627  fourierdlem97  46653  fourierdlem103  46659  fourierdlem104  46660  fourierdlem109  46665  sge00  46826  sge0sn  46829  sge0xaddlem2  46884  decsmf  47217  smflimsuplem1  47270  smflimsuplem3  47272  smflimsup  47278