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

Theorem negeq 9044
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 5866 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9040 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9040 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2340 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623  (class class class)co 5858   0cc0 8737    - cmin 9037   -ucneg 9038
This theorem is referenced by:  negeqi  9045  negeqd  9046  neg11  9098  renegcl  9110  infm3lem  9712  infm3  9713  riotaneg  9729  negiso  9730  infmsup  9732  infmrcl  9733  elz  10026  elz2  10040  znegcl  10055  zindd  10113  ublbneg  10302  eqreznegel  10303  negn0  10304  supminf  10305  zsupss  10307  qnegcl  10333  xnegeq  10534  expneg  11111  m1expcl2  11125  sqeqor  11217  sqrmo  11737  dvdsnegb  12546  pcexp  12912  pcneg  12926  mulgneg2  14594  negfcncf  18422  xrhmeo  18444  evth2  18458  volsup2  18960  mbfi1fseqlem2  19071  mbfi1fseq  19076  lhop2  19362  lognegb  19943  lgsdir2lem4  20565  rpvmasum2  20661  gxval  20925  gxnn0neg  20930  areacirc  24343  rexzrexnn0  26297  dvdsrabdioph  26303  monotoddzzfi  26439  monotoddzz  26440  oddcomabszz  26441  ceilingval  27617
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-iota 5219  df-fv 5263  df-ov 5861  df-neg 9040
  Copyright terms: Public domain W3C validator