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

Theorem negeq 9230
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 6028 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9226 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9226 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2444 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649  (class class class)co 6020   0cc0 8923    - cmin 9223   -ucneg 9224
This theorem is referenced by:  negeqi  9231  negeqd  9232  neg11  9284  renegcl  9296  infm3lem  9898  infm3  9899  riotaneg  9915  negiso  9916  infmsup  9918  infmrcl  9919  elz  10216  elz2  10230  znegcl  10245  zindd  10303  ublbneg  10492  eqreznegel  10493  negn0  10494  supminf  10495  zsupss  10497  qnegcl  10523  xnegeq  10725  expneg  11316  m1expcl2  11330  sqeqor  11422  sqrmo  11984  dvdsnegb  12794  pcexp  13160  pcneg  13174  mulgneg2  14844  negfcncf  18820  xrhmeo  18842  evth2  18856  volsup2  19364  mbfi1fseqlem2  19475  mbfi1fseq  19480  lhop2  19766  lognegb  20351  lgsdir2lem4  20977  rpvmasum2  21073  gxval  21694  gxnn0neg  21699  areacirc  25988  rexzrexnn0  26555  dvdsrabdioph  26561  monotoddzzfi  26696  monotoddzz  26697  oddcomabszz  26698  ceilingval  27874
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
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 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-rab 2658  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-uni 3958  df-br 4154  df-iota 5358  df-fv 5402  df-ov 6023  df-neg 9226
  Copyright terms: Public domain W3C validator