Theorem negeq 11355

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7349  0cc0 11009   − cmin 11347  -cneg 11348

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-iota 6438  df-fv 6490  df-ov 7352  df-neg 11350

This theorem is referenced by:  negeqi  11356  negeqd  11357  neg11  11415  renegcl  11427  negn0  11549  negf1o  11550  negfi  12074  infm3lem  12083  infm3  12084  riotaneg  12104  negiso  12105  infrenegsup  12108  elz  12473  elz2  12489  znegcl  12510  zindd  12577  zriotaneg  12589  ublbneg  12834  eqreznegel  12835  supminf  12836  zsupss  12838  qnegcl  12867  xnegeq  13109  ceilval  13742  expneg  13976  m1expcl2  13992  sqeqor  14123  sqrmo  15158  dvdsnegb  16184  lcmneg  16514  pcexp  16771  pcneg  16786  mulgneg2  18987  negfcncf  24815  xrhmeo  24842  evth2  24857  volsup2  25504  mbfi1fseqlem2  25615  mbfi1fseq  25620  lhop2  25918  lognegb  26497  lgsdir2lem4  27237  rpvmasum2  27421  ex-ceil  30392  elrgspnlem1  33182  hgt749d  34617  itgaddnclem2  37659  ftc1anclem5  37677  areacirc  37693  renegclALT  38942  rexzrexnn0  42777  dvdsrabdioph  42783  monotoddzzfi  42915  monotoddzz  42916  oddcomabszz  42917  infnsuprnmpt  45228  supminfrnmpt  45424  supminfxr  45443  etransclem17  46232  etransclem46  46261  etransclem47  46262  2zrngagrp  48233  digval  48583