Theorem negeq 11444

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

Syntax hints:   → wi 4   = wceq 1570  (class class class)co 7410  0cc0 11095   − cmin 11436  -cneg 11437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-iota 6492  df-fv 6544  df-ov 7413  df-neg 11439

This theorem is referenced by:  negeqi  11445  negeqd  11446  neg11  11504  renegcl  11516  negn0  11638  negf1o  11639  negfi  12159  infm3lem  12168  infm3  12169  riotaneg  12189  negiso  12190  infrenegsup  12193  elz  12588  elz2  12604  znegcl  12624  zindd  12692  zriotaneg  12704  ublbneg  12952  eqreznegel  12953  supminf  12954  zsupss  12956  qnegcl  12985  xnegeq  13228  ceilval  13867  expneg  14101  m1expcl2  14117  sqeqor  14248  sqrmo  15298  dvdsnegb  16326  lcmneg  16656  pcexp  16914  pcneg  16929  mulgneg2  19169  negfcncf  25082  xrhmeo  25105  evth2  25119  volsup2  25764  mbfi1fseqlem2  25875  mbfi1fseq  25880  lhop2  26174  lognegb  26755  lgsdir2lem4  27492  rpvmasum2  27676  ex-ceil  30799  elrgspnlem1  33562  hgt749d  35036  itgaddnclem2  38350  ftc1anclem5  38368  areacirc  38384  renegclALT  39757  rexzrexnn0  43551  dvdsrabdioph  43557  monotoddzzfi  43689  monotoddzz  43690  oddcomabszz  43691  infnsuprnmpt  45985  supminfrnmpt  46179  supminfxr  46198  etransclem17  46985  etransclem46  47014  etransclem47  47015  2zrngagrp  49034  digval  49398