Theorem negeq 11259

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

Syntax hints:   → wi 4   = wceq 1539  (class class class)co 7307  0cc0 10917   − cmin 11251  -cneg 11252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4566  df-pr 4568  df-op 4572  df-uni 4845  df-br 5082  df-iota 6410  df-fv 6466  df-ov 7310  df-neg 11254

This theorem is referenced by:  negeqi  11260  negeqd  11261  neg11  11318  renegcl  11330  negn0  11450  negf1o  11451  negfi  11970  infm3lem  11979  infm3  11980  riotaneg  12000  negiso  12001  infrenegsup  12004  elz  12367  elz2  12383  znegcl  12401  zindd  12467  zriotaneg  12481  ublbneg  12719  eqreznegel  12720  supminf  12721  zsupss  12723  qnegcl  12752  xnegeq  12987  ceilval  13604  expneg  13836  m1expcl2  13850  sqeqor  13978  sqrmo  15008  dvdsnegb  16028  lcmneg  16353  pcexp  16605  pcneg  16620  mulgneg2  18782  negfcncf  24131  xrhmeo  24154  evth2  24168  volsup2  24814  mbfi1fseqlem2  24926  mbfi1fseq  24931  lhop2  25224  lognegb  25790  lgsdir2lem4  26521  rpvmasum2  26705  ex-ceil  28857  hgt749d  32674  itgaddnclem2  35880  ftc1anclem5  35898  areacirc  35914  renegclALT  37019  rexzrexnn0  40663  dvdsrabdioph  40669  monotoddzzfi  40802  monotoddzz  40803  oddcomabszz  40804  infnsuprnmpt  42841  supminfrnmpt  43033  supminfxr  43052  etransclem17  43841  etransclem46  43870  etransclem47  43871  2zrngagrp  45559  digval  46002