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

Theorem negeq 9590
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 6088 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9586 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9586 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2490 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362  (class class class)co 6080   0cc0 9270    - cmin 9583   -ucneg 9584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-rex 2711  df-rab 2714  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-iota 5369  df-fv 5414  df-ov 6083  df-neg 9586
This theorem is referenced by:  negeqi  9591  negeqd  9592  neg11  9648  renegcl  9660  infm3lem  10276  infm3  10277  riotaneg  10293  negiso  10294  infmsup  10296  infmrcl  10297  elz  10636  elz2  10651  znegcl  10668  zindd  10731  zriotaneg  10742  ublbneg  10927  eqreznegel  10928  negn0  10929  supminf  10930  zsupss  10932  qnegcl  10958  xnegeq  11165  ceilval  11663  expneg  11857  m1expcl2  11871  sqeqor  11964  sqrmo  12725  dvdsnegb  13533  pcexp  13909  pcneg  13923  mulgneg2  15634  negfcncf  20337  xrhmeo  20360  evth2  20374  volsup2  20927  mbfi1fseqlem2  21036  mbfi1fseq  21041  lhop2  21329  lognegb  21923  lgsdir2lem4  22550  rpvmasum2  22646  gxval  23568  gxnn0neg  23573  itgaddnclem2  28295  ftc1anclem5  28315  areacirc  28333  rexzrexnn0  28987  dvdsrabdioph  28993  monotoddzzfi  29128  monotoddzz  29129  oddcomabszz  29130  renegclALT  32187
  Copyright terms: Public domain W3C validator