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

Theorem negeq 9254
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 6048 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9250 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9250 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2461 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649  (class class class)co 6040   0cc0 8946    - cmin 9247   -ucneg 9248
This theorem is referenced by:  negeqi  9255  negeqd  9256  neg11  9308  renegcl  9320  infm3lem  9922  infm3  9923  riotaneg  9939  negiso  9940  infmsup  9942  infmrcl  9943  elz  10240  elz2  10254  znegcl  10269  zindd  10327  ublbneg  10516  eqreznegel  10517  negn0  10518  supminf  10519  zsupss  10521  qnegcl  10547  xnegeq  10749  expneg  11344  m1expcl2  11358  sqeqor  11450  sqrmo  12012  dvdsnegb  12822  pcexp  13188  pcneg  13202  mulgneg2  14872  negfcncf  18902  xrhmeo  18924  evth2  18938  volsup2  19450  mbfi1fseqlem2  19561  mbfi1fseq  19566  lhop2  19852  lognegb  20437  lgsdir2lem4  21063  rpvmasum2  21159  gxval  21799  gxnn0neg  21804  itgaddnclem2  26163  areacirc  26187  rexzrexnn0  26754  dvdsrabdioph  26760  monotoddzzfi  26895  monotoddzz  26896  oddcomabszz  26897  ceilingval  28242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-iota 5377  df-fv 5421  df-ov 6043  df-neg 9250
  Copyright terms: Public domain W3C validator