Theorem negeq 10867

Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
negeq	⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)

Proof of Theorem negeq

Step	Hyp	Ref	Expression
1		oveq2 7143	. 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2		df-neg 10862	. 2 ⊢ -𝐴 = (0 − 𝐴)
3		df-neg 10862	. 2 ⊢ -𝐵 = (0 − 𝐵)
4	1, 2, 3	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1538  (class class class)co 7135  0cc0 10526   − cmin 10859  -cneg 10860

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-iota 6283  df-fv 6332  df-ov 7138  df-neg 10862

This theorem is referenced by:  negeqi  10868  negeqd  10869  neg11  10926  renegcl  10938  negn0  11058  negf1o  11059  negfi  11577  infm3lem  11586  infm3  11587  riotaneg  11607  negiso  11608  infrenegsup  11611  elz  11971  elz2  11987  znegcl  12005  zindd  12071  zriotaneg  12084  ublbneg  12321  eqreznegel  12322  supminf  12323  zsupss  12325  qnegcl  12353  xnegeq  12588  ceilval  13203  expneg  13433  m1expcl2  13447  sqeqor  13574  sqrmo  14603  dvdsnegb  15619  lcmneg  15937  pcexp  16186  pcneg  16200  mulgneg2  18253  negfcncf  23528  xrhmeo  23551  evth2  23565  volsup2  24209  mbfi1fseqlem2  24320  mbfi1fseq  24325  lhop2  24618  lognegb  25181  lgsdir2lem4  25912  rpvmasum2  26096  ex-ceil  28233  hgt749d  32030  itgaddnclem2  35116  ftc1anclem5  35134  areacirc  35150  renegclALT  36259  rexzrexnn0  39745  dvdsrabdioph  39751  monotoddzzfi  39883  monotoddzz  39884  oddcomabszz  39885  infnsuprnmpt  41888  supminfrnmpt  42082  supminfxr  42103  etransclem17  42893  etransclem46  42922  etransclem47  42923  2zrngagrp  44567  digval  45012