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

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

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 6643 . 2 (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2 df-neg 10254 . 2 -𝐴 = (0 − 𝐴)
3 df-neg 10254 . 2 -𝐵 = (0 − 𝐵)
41, 2, 33eqtr4g 2679 1 (𝐴 = 𝐵 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481  (class class class)co 6635  0cc0 9921  cmin 10251  -cneg 10252
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-rex 2915  df-rab 2918  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-uni 4428  df-br 4645  df-iota 5839  df-fv 5884  df-ov 6638  df-neg 10254
This theorem is referenced by:  negeqi  10259  negeqd  10260  neg11  10317  renegcl  10329  negn0  10444  negf1o  10445  negfi  10956  fiminre  10957  infm3lem  10966  infm3  10967  riotaneg  10987  negiso  10988  infrenegsup  10991  elz  11364  elz2  11379  znegcl  11397  zindd  11463  zriotaneg  11476  ublbneg  11758  eqreznegel  11759  supminf  11760  zsupss  11762  qnegcl  11790  xnegeq  12023  ceilval  12622  expneg  12851  m1expcl2  12865  sqeqor  12961  sqrmo  13973  dvdsnegb  14980  lcmneg  15297  pcexp  15545  pcneg  15559  mulgneg2  17556  negfcncf  22703  xrhmeo  22726  evth2  22740  volsup2  23354  mbfi1fseqlem2  23464  mbfi1fseq  23469  lhop2  23759  lognegb  24317  lgsdir2lem4  25034  rpvmasum2  25182  ex-ceil  27275  hgt749d  30701  itgaddnclem2  33440  ftc1anclem5  33460  areacirc  33476  renegclALT  34068  rexzrexnn0  37187  dvdsrabdioph  37193  monotoddzzfi  37326  monotoddzz  37327  oddcomabszz  37328  infnsuprnmpt  39281  supminfrnmpt  39485  supminfxr  39507  etransclem17  40231  etransclem46  40260  etransclem47  40261  2zrngagrp  41708  digval  42157
  Copyright terms: Public domain W3C validator