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

Theorem supeq1i 8899
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 8897 . 2 (𝐵 = 𝐶 → sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅))
31, 2ax-mp 5 1 sup(𝐵, 𝐴, 𝑅) = sup(𝐶, 𝐴, 𝑅)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  supcsup 8892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-ral 3140  df-rex 3141  df-rab 3144  df-uni 4831  df-sup 8894
This theorem is referenced by:  supsn  8924  infrenegsup  11612  supxrmnf  12698  rpsup  13222  resup  13223  gcdcom  15850  gcdass  15883  ovolgelb  24008  itg2seq  24270  itg2i1fseq  24283  itg2cnlem1  24289  dvfsumrlim  24555  pserdvlem2  24943  logtayl  25170  nmopnegi  29669  nmop0  29690  nmfn0  29691  esumnul  31206  ismblfin  34814  ovoliunnfl  34815  voliunnfl  34817  itg2addnclem  34824  binomcxplemdvsum  40564  binomcxp  40566  supxrleubrnmptf  41603  limsup0  41851  limsupresico  41857  liminfresico  41928  liminf10ex  41931  ioodvbdlimc1lem1  42092  ioodvbdlimc1  42094  ioodvbdlimc2  42096  fourierdlem41  42310  fourierdlem48  42316  fourierdlem49  42317  fourierdlem70  42338  fourierdlem71  42339  fourierdlem97  42365  fourierdlem103  42371  fourierdlem104  42372  fourierdlem109  42377  sge00  42535  sge0sn  42538  sge0xaddlem2  42593  decsmf  42920  smflimsuplem1  42971  smflimsuplem3  42973  smflimsup  42979
  Copyright terms: Public domain W3C validator