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

Theorem negeq 9060
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
negeq  |-  ( A  =  B  ->  -u A  =  -u B )

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 5882 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9056 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9056 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2353 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632  (class class class)co 5874   0cc0 8753    - cmin 9053   -ucneg 9054
This theorem is referenced by:  negeqi  9061  negeqd  9062  neg11  9114  renegcl  9126  infm3lem  9728  infm3  9729  riotaneg  9745  negiso  9746  infmsup  9748  infmrcl  9749  elz  10042  elz2  10056  znegcl  10071  zindd  10129  ublbneg  10318  eqreznegel  10319  negn0  10320  supminf  10321  zsupss  10323  qnegcl  10349  xnegeq  10550  expneg  11127  m1expcl2  11141  sqeqor  11233  sqrmo  11753  dvdsnegb  12562  pcexp  12928  pcneg  12942  mulgneg2  14610  negfcncf  18438  xrhmeo  18460  evth2  18474  volsup2  18976  mbfi1fseqlem2  19087  mbfi1fseq  19092  lhop2  19378  lognegb  19959  lgsdir2lem4  20581  rpvmasum2  20677  gxval  20941  gxnn0neg  20946  areacirc  25034  rexzrexnn0  26988  dvdsrabdioph  26994  monotoddzzfi  27130  monotoddzz  27131  oddcomabszz  27132  ceilingval  28509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-iota 5235  df-fv 5279  df-ov 5877  df-neg 9056
  Copyright terms: Public domain W3C validator