Theorem negeq 11385

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7367  0cc0 11038   − cmin 11377  -cneg 11378

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380

This theorem is referenced by:  negeqi  11386  negeqd  11387  neg11  11445  renegcl  11457  negn0  11579  negf1o  11580  negfi  12105  infm3lem  12114  infm3  12115  riotaneg  12135  negiso  12136  infrenegsup  12139  elz  12526  elz2  12542  znegcl  12562  zindd  12630  zriotaneg  12642  ublbneg  12883  eqreznegel  12884  supminf  12885  zsupss  12887  qnegcl  12916  xnegeq  13159  ceilval  13797  expneg  14031  m1expcl2  14047  sqeqor  14178  sqrmo  15213  dvdsnegb  16242  lcmneg  16572  pcexp  16830  pcneg  16845  mulgneg2  19084  negfcncf  24890  xrhmeo  24913  evth2  24927  volsup2  25572  mbfi1fseqlem2  25683  mbfi1fseq  25688  lhop2  25982  lognegb  26554  lgsdir2lem4  27291  rpvmasum2  27475  ex-ceil  30518  elrgspnlem1  33303  hgt749d  34793  itgaddnclem2  38000  ftc1anclem5  38018  areacirc  38034  renegclALT  39409  rexzrexnn0  43232  dvdsrabdioph  43238  monotoddzzfi  43370  monotoddzz  43371  oddcomabszz  43372  infnsuprnmpt  45679  supminfrnmpt  45873  supminfxr  45892  etransclem17  46679  etransclem46  46708  etransclem47  46709  2zrngagrp  48725  digval  49074