Theorem negeq 11422

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

Syntax hints:   → wi 4   = wceq 1560  (class class class)co 7396  0cc0 11073   − cmin 11414  -cneg 11415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-neg 11417

This theorem is referenced by:  negeqi  11423  negeqd  11424  neg11  11482  renegcl  11494  negn0  11616  negf1o  11617  negfi  12141  infm3lem  12150  infm3  12151  riotaneg  12171  negiso  12172  infrenegsup  12175  elz  12570  elz2  12586  znegcl  12606  zindd  12674  zriotaneg  12686  ublbneg  12934  eqreznegel  12935  supminf  12936  zsupss  12938  qnegcl  12967  xnegeq  13210  ceilval  13848  expneg  14082  m1expcl2  14098  sqeqor  14229  sqrmo  15278  dvdsnegb  16307  lcmneg  16637  pcexp  16895  pcneg  16910  mulgneg2  19150  negfcncf  24985  xrhmeo  25008  evth2  25022  volsup2  25667  mbfi1fseqlem2  25778  mbfi1fseq  25783  lhop2  26077  lognegb  26655  lgsdir2lem4  27392  rpvmasum2  27576  ex-ceil  30650  elrgspnlem1  33423  hgt749d  34943  itgaddnclem2  38178  ftc1anclem5  38196  areacirc  38212  renegclALT  39587  rexzrexnn0  43381  dvdsrabdioph  43387  monotoddzzfi  43519  monotoddzz  43520  oddcomabszz  43521  infnsuprnmpt  45825  supminfrnmpt  46019  supminfxr  46038  etransclem17  46825  etransclem46  46854  etransclem47  46855  2zrngagrp  48871  digval  49220