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

Theorem negeq 9808
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 6290 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9804 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9804 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2533 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1379  (class class class)co 6282   0cc0 9488    - cmin 9801   -ucneg 9802
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-or 370  df-an 371  df-3an 975  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-rex 2820  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-iota 5549  df-fv 5594  df-ov 6285  df-neg 9804
This theorem is referenced by:  negeqi  9809  negeqd  9810  neg11  9866  renegcl  9878  infm3lem  10497  infm3  10498  riotaneg  10514  negiso  10515  infmsup  10517  infmrcl  10518  elz  10862  elz2  10877  znegcl  10894  zindd  10958  zriotaneg  10970  ublbneg  11162  eqreznegel  11163  negn0  11164  supminf  11165  zsupss  11167  qnegcl  11195  xnegeq  11402  ceilval  11930  expneg  12137  m1expcl2  12151  sqeqor  12244  sqrmo  13042  dvdsnegb  13855  pcexp  14235  pcneg  14249  mulgneg2  15966  negfcncf  21155  xrhmeo  21178  evth2  21192  volsup2  21746  mbfi1fseqlem2  21855  mbfi1fseq  21860  lhop2  22148  lognegb  22699  lgsdir2lem4  23326  rpvmasum2  23422  gxval  24933  gxnn0neg  24938  itgaddnclem2  29649  ftc1anclem5  29669  areacirc  29687  rexzrexnn0  30339  dvdsrabdioph  30345  monotoddzzfi  30480  monotoddzz  30481  oddcomabszz  30482  lcmneg  30809  fourierdlem39  31446  renegclALT  33766
  Copyright terms: Public domain W3C validator