Theorem negeq 11389

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7369  0cc0 11044   − cmin 11381  -cneg 11382

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-neg 11384

This theorem is referenced by:  negeqi  11390  negeqd  11391  neg11  11449  renegcl  11461  negn0  11583  negf1o  11584  negfi  12108  infm3lem  12117  infm3  12118  riotaneg  12138  negiso  12139  infrenegsup  12142  elz  12507  elz2  12523  znegcl  12544  zindd  12611  zriotaneg  12623  ublbneg  12868  eqreznegel  12869  supminf  12870  zsupss  12872  qnegcl  12901  xnegeq  13143  ceilval  13776  expneg  14010  m1expcl2  14026  sqeqor  14157  sqrmo  15193  dvdsnegb  16219  lcmneg  16549  pcexp  16806  pcneg  16821  mulgneg2  19022  negfcncf  24850  xrhmeo  24877  evth2  24892  volsup2  25539  mbfi1fseqlem2  25650  mbfi1fseq  25655  lhop2  25953  lognegb  26532  lgsdir2lem4  27272  rpvmasum2  27456  ex-ceil  30427  elrgspnlem1  33209  hgt749d  34633  itgaddnclem2  37666  ftc1anclem5  37684  areacirc  37700  renegclALT  38949  rexzrexnn0  42785  dvdsrabdioph  42791  monotoddzzfi  42924  monotoddzz  42925  oddcomabszz  42926  infnsuprnmpt  45237  supminfrnmpt  45434  supminfxr  45453  etransclem17  46242  etransclem46  46271  etransclem47  46272  2zrngagrp  48230  digval  48580