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

Theorem supeq1i 7903
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 7901 . 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 1379   supcsup 7896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-rex 2820  df-rab 2823  df-uni 4246  df-sup 7897
This theorem is referenced by:  supsn  7926  infmsup  10517  nninfm  11158  nn0infm  11159  supxrmnf  11505  rpsup  11957  resup  11958  gcdcom  14013  gcdass  14038  imasdsval2  14767  imasdsf1olem  20611  ovolgelb  21626  itg2seq  21884  itg2i1fseq  21897  itg2cnlem1  21903  dvfsumrlim  22167  pserdvlem2  22557  logtayl  22769  ftalem6  23079  nmopnegi  26560  nmop0  26581  nmfn0  26582  esumnul  27699  ismblfin  29632  ovoliunnfl  29633  voliunnfl  29635  itg2addnclem  29643  lcmcom  30799  lcmass  30818  ioodvbdlimc1lem1  31261  ioodvbdlimc1lem2  31262  ioodvbdlimc1  31263  ioodvbdlimc2lem  31264  ioodvbdlimc2  31265  fourierdlem41  31448  fourierdlem45  31452  fourierdlem48  31455  fourierdlem49  31456  fourierdlem70  31477  fourierdlem71  31478  fourierdlem97  31504  fourierdlem103  31510  fourierdlem104  31511
  Copyright terms: Public domain W3C validator