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

Theorem negeq 9089
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 5908 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9085 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9085 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2373 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633  (class class class)co 5900   0cc0 8782    - cmin 9082   -ucneg 9083
This theorem is referenced by:  negeqi  9090  negeqd  9091  neg11  9143  renegcl  9155  infm3lem  9757  infm3  9758  riotaneg  9774  negiso  9775  infmsup  9777  infmrcl  9778  elz  10073  elz2  10087  znegcl  10102  zindd  10160  ublbneg  10349  eqreznegel  10350  negn0  10351  supminf  10352  zsupss  10354  qnegcl  10380  xnegeq  10581  expneg  11158  m1expcl2  11172  sqeqor  11264  sqrmo  11784  dvdsnegb  12593  pcexp  12959  pcneg  12973  mulgneg2  14643  negfcncf  18475  xrhmeo  18497  evth2  18511  volsup2  19013  mbfi1fseqlem2  19124  mbfi1fseq  19129  lhop2  19415  lognegb  19996  lgsdir2lem4  20618  rpvmasum2  20714  gxval  20978  gxnn0neg  20983  areacirc  25348  rexzrexnn0  26033  dvdsrabdioph  26039  monotoddzzfi  26175  monotoddzz  26176  oddcomabszz  26177  ceilingval  27704
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-sn 3680  df-pr 3681  df-op 3683  df-uni 3865  df-br 4061  df-iota 5256  df-fv 5300  df-ov 5903  df-neg 9085
  Copyright terms: Public domain W3C validator