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

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

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 6439 . 2 (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2 df-neg 10024 . 2 -𝐴 = (0 − 𝐴)
3 df-neg 10024 . 2 -𝐵 = (0 − 𝐵)
41, 2, 33eqtr4g 2573 1 (𝐴 = 𝐵 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  (class class class)co 6431  0cc0 9695  cmin 10021  -cneg 10022
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-rex 2806  df-rab 2809  df-v 3079  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-uni 4271  df-br 4482  df-iota 5658  df-fv 5702  df-ov 6434  df-neg 10024
This theorem is referenced by:  negeqi  10029  negeqd  10030  neg11  10087  renegcl  10099  negn0  10214  negf1o  10215  negfi  10725  fiminre  10726  infm3lem  10738  infm3  10739  riotaneg  10757  negiso  10758  infrenegsup  10761  infmsupOLD  10762  infmrclOLD  10763  elz  11124  elz2  11139  znegcl  11157  zindd  11222  zriotaneg  11235  ublbneg  11519  eqreznegel  11520  supminf  11521  zsupss  11523  qnegcl  11551  xnegeq  11785  ceilval  12373  expneg  12602  m1expcl2  12616  sqeqor  12712  sqrmo  13703  dvdsnegb  14710  lcmneg  15034  pcexp  15290  pcneg  15304  mulgneg2  17294  negfcncf  22457  xrhmeo  22480  evth2  22494  volsup2  23058  mbfi1fseqlem2  23168  mbfi1fseq  23173  lhop2  23461  lognegb  24031  lgsdir2lem4  24746  rpvmasum2  24894  ex-ceil  26439  itgaddnclem2  32533  ftc1anclem5  32553  areacirc  32569  renegclALT  33161  rexzrexnn0  36280  dvdsrabdioph  36286  monotoddzzfi  36419  monotoddzz  36420  oddcomabszz  36421  etransclem17  39054  etransclem46  39083  etransclem47  39084  2zrngagrp  41842  digval  42299
  Copyright terms: Public domain W3C validator