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

Theorem negeq 9594
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 6094 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 9590 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 9590 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2495 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369  (class class class)co 6086   0cc0 9274    - cmin 9587   -ucneg 9588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-iota 5376  df-fv 5421  df-ov 6089  df-neg 9590
This theorem is referenced by:  negeqi  9595  negeqd  9596  neg11  9652  renegcl  9664  infm3lem  10280  infm3  10281  riotaneg  10297  negiso  10298  infmsup  10300  infmrcl  10301  elz  10640  elz2  10655  znegcl  10672  zindd  10735  zriotaneg  10746  ublbneg  10931  eqreznegel  10932  negn0  10933  supminf  10934  zsupss  10936  qnegcl  10962  xnegeq  11169  ceilval  11671  expneg  11865  m1expcl2  11879  sqeqor  11972  sqrmo  12733  dvdsnegb  13542  pcexp  13918  pcneg  13932  mulgneg2  15645  negfcncf  20475  xrhmeo  20498  evth2  20512  volsup2  21065  mbfi1fseqlem2  21174  mbfi1fseq  21179  lhop2  21467  lognegb  22018  lgsdir2lem4  22645  rpvmasum2  22741  gxval  23713  gxnn0neg  23718  itgaddnclem2  28422  ftc1anclem5  28442  areacirc  28460  rexzrexnn0  29113  dvdsrabdioph  29119  monotoddzzfi  29254  monotoddzz  29255  oddcomabszz  29256  renegclALT  32507
  Copyright terms: Public domain W3C validator