Theorem negeq 11489

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 7427	. 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵))
2		df-neg 11484	. 2 ⊢ -𝐴 = (0 − 𝐴)
3		df-neg 11484	. 2 ⊢ -𝐵 = (0 − 𝐵)
4	1, 2, 3	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵)

Syntax hints:   → wi 4   = wceq 1533  (class class class)co 7419  0cc0 11145   − cmin 11481  -cneg 11482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-iota 6501  df-fv 6557  df-ov 7422  df-neg 11484

This theorem is referenced by:  negeqi  11490  negeqd  11491  neg11  11548  renegcl  11560  negn0  11680  negf1o  11681  negfi  12201  infm3lem  12210  infm3  12211  riotaneg  12231  negiso  12232  infrenegsup  12235  elz  12598  elz2  12614  znegcl  12635  zindd  12701  zriotaneg  12713  ublbneg  12955  eqreznegel  12956  supminf  12957  zsupss  12959  qnegcl  12988  xnegeq  13226  ceilval  13844  expneg  14075  m1expcl2  14091  sqeqor  14220  sqrmo  15239  dvdsnegb  16259  lcmneg  16582  pcexp  16836  pcneg  16851  mulgneg2  19076  negfcncf  24893  xrhmeo  24920  evth2  24935  volsup2  25583  mbfi1fseqlem2  25695  mbfi1fseq  25700  lhop2  25997  lognegb  26574  lgsdir2lem4  27311  rpvmasum2  27495  ex-ceil  30335  hgt749d  34414  itgaddnclem2  37285  ftc1anclem5  37303  areacirc  37319  renegclALT  38567  rexzrexnn0  42368  dvdsrabdioph  42374  monotoddzzfi  42507  monotoddzz  42508  oddcomabszz  42509  infnsuprnmpt  44766  supminfrnmpt  44967  supminfxr  44986  etransclem17  45779  etransclem46  45808  etransclem47  45809  2zrngagrp  47499  digval  47859