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

Theorem supeq1i 7940
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 7938 . 2  |-  ( B  =  C  ->  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R ) )
31, 2ax-mp 5 1  |-  sup ( B ,  A ,  R )  =  sup ( C ,  A ,  R )
Colors of variables: wff setvar class
Syntax hints:    = wceq 1405   supcsup 7934
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ral 2759  df-rex 2760  df-rab 2763  df-uni 4192  df-sup 7935
This theorem is referenced by:  supsn  7964  infmsup  10561  nninfm  11207  nn0infm  11208  supxrmnf  11562  rpsup  12031  resup  12032  gcdcom  14367  gcdass  14392  imasdsval2  15130  imasdsf1olem  21168  ovolgelb  22183  itg2seq  22441  itg2i1fseq  22454  itg2cnlem1  22460  dvfsumrlim  22724  pserdvlem2  23115  logtayl  23335  ftalem6  23732  nmopnegi  27297  nmop0  27318  nmfn0  27319  esumnul  28495  ismblfin  31427  ovoliunnfl  31428  voliunnfl  31430  itg2addnclem  31439  lcmcom  36047  lcmass  36066  binomcxplemdvsum  36108  binomcxp  36110  ioodvbdlimc1lem1  37096  ioodvbdlimc1lem2  37097  ioodvbdlimc1  37098  ioodvbdlimc2lem  37099  ioodvbdlimc2  37100  fourierdlem41  37298  fourierdlem48  37305  fourierdlem49  37306  fourierdlem70  37327  fourierdlem71  37328  fourierdlem97  37354  fourierdlem103  37360  fourierdlem104  37361  fourierdlem109  37366  elaa2  37385  etransc  37434
  Copyright terms: Public domain W3C validator