Theorem negeq 11449

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

Syntax hints:   → wi 4   = wceq 1567  (class class class)co 7411  0cc0 11100   − cmin 11441  -cneg 11442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-iota 6493  df-fv 6545  df-ov 7414  df-neg 11444

This theorem is referenced by:  negeqi  11450  negeqd  11451  neg11  11509  renegcl  11521  negn0  11643  negf1o  11644  negfi  12164  infm3lem  12173  infm3  12174  riotaneg  12194  negiso  12195  infrenegsup  12198  elz  12593  elz2  12609  znegcl  12629  zindd  12697  zriotaneg  12709  ublbneg  12957  eqreznegel  12958  supminf  12959  zsupss  12961  qnegcl  12990  xnegeq  13233  ceilval  13871  expneg  14105  m1expcl2  14121  sqeqor  14252  sqrmo  15302  dvdsnegb  16331  lcmneg  16661  pcexp  16919  pcneg  16934  mulgneg2  19174  negfcncf  25051  xrhmeo  25074  evth2  25088  volsup2  25733  mbfi1fseqlem2  25844  mbfi1fseq  25849  lhop2  26143  lognegb  26721  lgsdir2lem4  27458  rpvmasum2  27642  ex-ceil  30740  elrgspnlem1  33503  hgt749d  34981  itgaddnclem2  38218  ftc1anclem5  38236  areacirc  38252  renegclALT  39627  rexzrexnn0  43423  dvdsrabdioph  43429  monotoddzzfi  43561  monotoddzz  43562  oddcomabszz  43563  infnsuprnmpt  45857  supminfrnmpt  46051  supminfxr  46070  etransclem17  46857  etransclem46  46886  etransclem47  46887  2zrngagrp  48903  digval  49263