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

Theorem supeq1i 7200
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
StepHypRef Expression
1 supeq1i.1 . 2  |-  B  =  C
2 supeq1 7198 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2ax-mp 8 1  |-  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
Colors of variables: wff set class
Syntax hints:    = wceq 1623   supcsup 7193
This theorem is referenced by:  supsn  7220  infmsup  9732  nninfm  10298  nn0infm  10299  supxrmnf  10636  rpsup  10970  resup  10971  gcdcom  12699  gcdass  12724  imasdsval2  13419  imasdsf1olem  17937  ovolgelb  18839  itg2seq  19097  itg2i1fseq  19110  itg2cnlem1  19116  dvfsumrlim  19378  pserdvlem2  19804  logtayl  20007  ftalem6  20315  nmopnegi  22545  nmop0  22566  nmfn0  22567  esumnul  23427
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-rex 2549  df-rab 2552  df-uni 3828  df-sup 7194
  Copyright terms: Public domain W3C validator