Theorem negeq 11372

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

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7358  0cc0 11026   − cmin 11364  -cneg 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367

This theorem is referenced by:  negeqi  11373  negeqd  11374  neg11  11432  renegcl  11444  negn0  11566  negf1o  11567  negfi  12091  infm3lem  12100  infm3  12101  riotaneg  12121  negiso  12122  infrenegsup  12125  elz  12490  elz2  12506  znegcl  12526  zindd  12593  zriotaneg  12605  ublbneg  12846  eqreznegel  12847  supminf  12848  zsupss  12850  qnegcl  12879  xnegeq  13122  ceilval  13758  expneg  13992  m1expcl2  14008  sqeqor  14139  sqrmo  15174  dvdsnegb  16200  lcmneg  16530  pcexp  16787  pcneg  16802  mulgneg2  19038  negfcncf  24873  xrhmeo  24900  evth2  24915  volsup2  25562  mbfi1fseqlem2  25673  mbfi1fseq  25678  lhop2  25976  lognegb  26555  lgsdir2lem4  27295  rpvmasum2  27479  ex-ceil  30523  elrgspnlem1  33324  hgt749d  34806  itgaddnclem2  37880  ftc1anclem5  37898  areacirc  37914  renegclALT  39223  rexzrexnn0  43046  dvdsrabdioph  43052  monotoddzzfi  43184  monotoddzz  43185  oddcomabszz  43186  infnsuprnmpt  45494  supminfrnmpt  45689  supminfxr  45708  etransclem17  46495  etransclem46  46524  etransclem47  46525  2zrngagrp  48495  digval  48844