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

Theorem negeq 8998
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 5786 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 8994 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 8994 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2313 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1619  (class class class)co 5778   0cc0 8691    - cmin 8991   -ucneg 8992
This theorem is referenced by:  negeqi  8999  negeqd  9000  neg11  9052  renegcl  9064  infm3lem  9666  infm3  9667  riotaneg  9683  negiso  9684  infmsup  9686  infmrcl  9687  elz  9979  elz2  9993  znegcl  10008  zindd  10066  ublbneg  10255  eqreznegel  10256  negn0  10257  supminf  10258  zsupss  10260  qnegcl  10286  xnegeq  10486  expneg  11063  m1expcl2  11077  sqeqor  11169  sqrmo  11688  dvdsnegb  12494  pcexp  12860  pcneg  12874  mulgneg2  14542  negfcncf  18370  xrhmeo  18392  evth2  18406  volsup2  18908  mbfi1fseqlem2  19019  mbfi1fseq  19024  lhop2  19310  lognegb  19891  lgsdir2lem4  20513  rpvmasum2  20609  gxval  20871  gxnn0neg  20876  rexzrexnn0  26238  dvdsrabdioph  26244  monotoddzzfi  26380  monotoddzz  26381  oddcomabszz  26382  ceilingval  27288
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-xp 4661  df-cnv 4663  df-dm 4665  df-rn 4666  df-res 4667  df-ima 4668  df-fv 4675  df-ov 5781  df-neg 8994
  Copyright terms: Public domain W3C validator