Theorem supeq1i 8236

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

Syntax hints:   = wceq 1475  supcsup 8229

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-uni 4373  df-sup 8231

This theorem is referenced by:  supsn  8261  infrenegsup  10883  supxrmnf  12019  rpsup  12527  resup  12528  gcdcom  15073  gcdass  15102  ovolgelb  23055  itg2seq  23315  itg2i1fseq  23328  itg2cnlem1  23334  dvfsumrlim  23598  pserdvlem2  23986  logtayl  24206  nmopnegi  28208  nmop0  28229  nmfn0  28230  esumnul  29437  ismblfin  32620  ovoliunnfl  32621  voliunnfl  32623  itg2addnclem  32631  binomcxplemdvsum  37576  binomcxp  37578  ioodvbdlimc1lem1  38821  ioodvbdlimc1  38823  ioodvbdlimc2  38825  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem70  39069  fourierdlem71  39070  fourierdlem97  39096  fourierdlem103  39102  fourierdlem104  39103  fourierdlem109  39108  sge00  39269  sge0sn  39272  sge0xaddlem2  39327  decsmf  39653