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  19016  negfcncf  24793  xrhmeo  24820  evth2  24835  volsup2  25482  mbfi1fseqlem2  25593  mbfi1fseq  25598  lhop2  25896  lognegb  26475  lgsdir2lem4  27215  rpvmasum2  27399  ex-ceil  30350  elrgspnlem1  33166  hgt749d  34613  itgaddnclem2  37646  ftc1anclem5  37664  areacirc  37680  renegclALT  38929  rexzrexnn0  42765  dvdsrabdioph  42771  monotoddzzfi  42904  monotoddzz  42905  oddcomabszz  42906  infnsuprnmpt  45217  supminfrnmpt  45414  supminfxr  45433  etransclem17  46222  etransclem46  46251  etransclem47  46252  2zrngagrp  48210  digval  48560