Theorem negeq 11370

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

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7356  0cc0 11024   − cmin 11362  -cneg 11363

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-iota 6446  df-fv 6498  df-ov 7359  df-neg 11365

This theorem is referenced by:  negeqi  11371  negeqd  11372  neg11  11430  renegcl  11442  negn0  11564  negf1o  11565  negfi  12089  infm3lem  12098  infm3  12099  riotaneg  12119  negiso  12120  infrenegsup  12123  elz  12488  elz2  12504  znegcl  12524  zindd  12591  zriotaneg  12603  ublbneg  12844  eqreznegel  12845  supminf  12846  zsupss  12848  qnegcl  12877  xnegeq  13120  ceilval  13756  expneg  13990  m1expcl2  14006  sqeqor  14137  sqrmo  15172  dvdsnegb  16198  lcmneg  16528  pcexp  16785  pcneg  16800  mulgneg2  19036  negfcncf  24871  xrhmeo  24898  evth2  24913  volsup2  25560  mbfi1fseqlem2  25671  mbfi1fseq  25676  lhop2  25974  lognegb  26553  lgsdir2lem4  27293  rpvmasum2  27477  ex-ceil  30472  elrgspnlem1  33273  hgt749d  34755  itgaddnclem2  37819  ftc1anclem5  37837  areacirc  37853  renegclALT  39162  rexzrexnn0  42988  dvdsrabdioph  42994  monotoddzzfi  43126  monotoddzz  43127  oddcomabszz  43128  infnsuprnmpt  45436  supminfrnmpt  45631  supminfxr  45650  etransclem17  46437  etransclem46  46466  etransclem47  46467  2zrngagrp  48437  digval  48786