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

Theorem negeq 10866
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)
Assertion
Ref Expression
negeq (𝐴 = 𝐵 → -𝐴 = -𝐵)

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 7153 . 2 (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2 df-neg 10861 . 2 -𝐴 = (0 − 𝐴)
3 df-neg 10861 . 2 -𝐵 = (0 − 𝐵)
41, 2, 33eqtr4g 2878 1 (𝐴 = 𝐵 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  (class class class)co 7145  0cc0 10525  cmin 10858  -cneg 10859
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-iota 6307  df-fv 6356  df-ov 7148  df-neg 10861
This theorem is referenced by:  negeqi  10867  negeqd  10868  neg11  10925  renegcl  10937  negn0  11057  negf1o  11058  negfi  11577  fiminreOLD  11578  infm3lem  11587  infm3  11588  riotaneg  11608  negiso  11609  infrenegsup  11612  elz  11971  elz2  11987  znegcl  12005  zindd  12071  zriotaneg  12084  ublbneg  12321  eqreznegel  12322  supminf  12323  zsupss  12325  qnegcl  12353  xnegeq  12588  ceilval  13196  expneg  13425  m1expcl2  13439  sqeqor  13566  sqrmo  14599  dvdsnegb  15615  lcmneg  15935  pcexp  16184  pcneg  16198  mulgneg2  18199  negfcncf  23454  xrhmeo  23477  evth2  23491  volsup2  24133  mbfi1fseqlem2  24244  mbfi1fseq  24249  lhop2  24539  lognegb  25100  lgsdir2lem4  25831  rpvmasum2  26015  ex-ceil  28154  hgt749d  31819  itgaddnclem2  34832  ftc1anclem5  34852  areacirc  34868  renegclALT  35979  rexzrexnn0  39279  dvdsrabdioph  39285  monotoddzzfi  39417  monotoddzz  39418  oddcomabszz  39419  infnsuprnmpt  41398  supminfrnmpt  41595  supminfxr  41616  etransclem17  42413  etransclem46  42442  etransclem47  42443  2zrngagrp  44142  digval  44586
  Copyright terms: Public domain W3C validator