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

Theorem negeq 9875
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 6314 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9871 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9871 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2488 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437  (class class class)co 6306   0cc0 9547    - cmin 9868   -ucneg 9869
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-iota 5565  df-fv 5609  df-ov 6309  df-neg 9871
This theorem is referenced by:  negeqi  9876  negeqd  9877  neg11  9933  renegcl  9945  negn0  10056  negf1o  10057  negfi  10562  fiminre  10563  infm3lem  10575  infm3  10576  riotaneg  10594  negiso  10595  infrenegsup  10599  infmsupOLD  10600  infmrclOLD  10601  elz  10947  elz2  10962  znegcl  10980  zindd  11044  zriotaneg  11057  ublbneg  11256  eqreznegel  11257  supminf  11258  supminfOLD  11259  zsupss  11261  qnegcl  11289  xnegeq  11508  ceilval  12074  expneg  12287  m1expcl2  12301  sqeqor  12395  sqrmo  13316  dvdsnegb  14320  lcmneg  14568  pcexp  14809  pcneg  14823  mulgneg2  16785  negfcncf  21950  xrhmeo  21973  evth2  21987  volsup2  22562  mbfi1fseqlem2  22673  mbfi1fseq  22678  lhop2  22966  lognegb  23538  lgsdir2lem4  24253  rpvmasum2  24349  gxval  25985  gxnn0neg  25990  itgaddnclem2  31966  ftc1anclem5  31986  areacirc  32002  renegclALT  32505  rexzrexnn0  35617  dvdsrabdioph  35623  monotoddzzfi  35761  monotoddzz  35762  oddcomabszz  35763  etransclem17  38057  etransclem46  38086  etransclem47  38087  2zrngagrp  39592  digval  40060
  Copyright terms: Public domain W3C validator