MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  supeq1i Structured version   Visualization version   GIF version

Theorem supeq1i 8298
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
StepHypRef Expression
1 supeq1i.1 . 2 𝐵 = 𝐶
2 supeq1 8296 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1480  supcsup 8291
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ral 2917  df-rex 2918  df-rab 2921  df-uni 4408  df-sup 8293
This theorem is referenced by:  supsn  8323  infrenegsup  10951  supxrmnf  12087  rpsup  12602  resup  12603  gcdcom  15154  gcdass  15183  ovolgelb  23150  itg2seq  23410  itg2i1fseq  23423  itg2cnlem1  23429  dvfsumrlim  23693  pserdvlem2  24081  logtayl  24301  nmopnegi  28664  nmop0  28685  nmfn0  28686  esumnul  29883  ismblfin  33068  ovoliunnfl  33069  voliunnfl  33071  itg2addnclem  33079  binomcxplemdvsum  38022  binomcxp  38024  limsup0  39317  limsupresico  39323  ioodvbdlimc1lem1  39439  ioodvbdlimc1  39441  ioodvbdlimc2  39443  fourierdlem41  39659  fourierdlem48  39665  fourierdlem49  39666  fourierdlem70  39687  fourierdlem71  39688  fourierdlem97  39714  fourierdlem103  39720  fourierdlem104  39721  fourierdlem109  39726  sge00  39887  sge0sn  39890  sge0xaddlem2  39945  decsmf  40269  smflimsuplem1  40320  smflimsuplem3  40322  smflimsup  40328
  Copyright terms: Public domain W3C validator