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

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

Proof of Theorem negeq
StepHypRef Expression
1 oveq2 7138 . 2 (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2 df-neg 10850 . 2 -𝐴 = (0 − 𝐴)
3 df-neg 10850 . 2 -𝐵 = (0 − 𝐵)
41, 2, 33eqtr4g 2881 1 (𝐴 = 𝐵 → -𝐴 = -𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  (class class class)co 7130  0cc0 10514  cmin 10847  -cneg 10848
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-iota 6287  df-fv 6336  df-ov 7133  df-neg 10850
This theorem is referenced by:  negeqi  10856  negeqd  10857  neg11  10914  renegcl  10926  negn0  11046  negf1o  11047  negfi  11566  fiminreOLD  11567  infm3lem  11576  infm3  11577  riotaneg  11597  negiso  11598  infrenegsup  11601  elz  11961  elz2  11977  znegcl  11995  zindd  12061  zriotaneg  12074  ublbneg  12311  eqreznegel  12312  supminf  12313  zsupss  12315  qnegcl  12343  xnegeq  12578  ceilval  13191  expneg  13421  m1expcl2  13435  sqeqor  13562  sqrmo  14590  dvdsnegb  15606  lcmneg  15924  pcexp  16173  pcneg  16187  mulgneg2  18240  negfcncf  23507  xrhmeo  23530  evth2  23544  volsup2  24188  mbfi1fseqlem2  24299  mbfi1fseq  24304  lhop2  24597  lognegb  25160  lgsdir2lem4  25891  rpvmasum2  26075  ex-ceil  28212  hgt749d  31928  itgaddnclem2  35002  ftc1anclem5  35020  areacirc  35036  renegclALT  36145  rexzrexnn0  39556  dvdsrabdioph  39562  monotoddzzfi  39694  monotoddzz  39695  oddcomabszz  39696  infnsuprnmpt  41708  supminfrnmpt  41905  supminfxr  41926  etransclem17  42716  etransclem46  42745  etransclem47  42746  2zrngagrp  44390  digval  44834
  Copyright terms: Public domain W3C validator