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

Theorem negeq 9282
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 6075 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9278 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9278 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2487 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652  (class class class)co 6067   0cc0 8974    - cmin 9275   -ucneg 9276
This theorem is referenced by:  negeqi  9283  negeqd  9284  neg11  9336  renegcl  9348  infm3lem  9950  infm3  9951  riotaneg  9967  negiso  9968  infmsup  9970  infmrcl  9971  elz  10268  elz2  10282  znegcl  10297  zindd  10355  ublbneg  10544  eqreznegel  10545  negn0  10546  supminf  10547  zsupss  10549  qnegcl  10575  xnegeq  10777  expneg  11372  m1expcl2  11386  sqeqor  11478  sqrmo  12040  dvdsnegb  12850  pcexp  13216  pcneg  13230  mulgneg2  14900  negfcncf  18932  xrhmeo  18954  evth2  18968  volsup2  19480  mbfi1fseqlem2  19591  mbfi1fseq  19596  lhop2  19882  lognegb  20467  lgsdir2lem4  21093  rpvmasum2  21189  gxval  21829  gxnn0neg  21834  itgaddnclem2  26205  areacirc  26229  rexzrexnn0  26796  dvdsrabdioph  26802  monotoddzzfi  26937  monotoddzz  26938  oddcomabszz  26939  ceilingval  28284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-rex 2698  df-rab 2701  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810  df-uni 4003  df-br 4200  df-iota 5404  df-fv 5448  df-ov 6070  df-neg 9278
  Copyright terms: Public domain W3C validator