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

Theorem negeq 9712
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 6207 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9708 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9708 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2520 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370  (class class class)co 6199   0cc0 9392    - cmin 9705   -ucneg 9706
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-rex 2804  df-rab 2807  df-v 3078  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-iota 5488  df-fv 5533  df-ov 6202  df-neg 9708
This theorem is referenced by:  negeqi  9713  negeqd  9714  neg11  9770  renegcl  9782  infm3lem  10398  infm3  10399  riotaneg  10415  negiso  10416  infmsup  10418  infmrcl  10419  elz  10758  elz2  10773  znegcl  10790  zindd  10853  zriotaneg  10864  ublbneg  11049  eqreznegel  11050  negn0  11051  supminf  11052  zsupss  11054  qnegcl  11080  xnegeq  11287  ceilval  11795  expneg  11989  m1expcl2  12003  sqeqor  12096  sqrmo  12858  dvdsnegb  13667  pcexp  14043  pcneg  14057  mulgneg2  15772  negfcncf  20626  xrhmeo  20649  evth2  20663  volsup2  21217  mbfi1fseqlem2  21326  mbfi1fseq  21331  lhop2  21619  lognegb  22170  lgsdir2lem4  22797  rpvmasum2  22893  gxval  23896  gxnn0neg  23901  itgaddnclem2  28598  ftc1anclem5  28618  areacirc  28636  rexzrexnn0  29289  dvdsrabdioph  29295  monotoddzzfi  29430  monotoddzz  29431  oddcomabszz  29432  renegclALT  32937
  Copyright terms: Public domain W3C validator