Theorem negeq 11384

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

Syntax hints:   → wi 4   = wceq 1542  (class class class)co 7368  0cc0 11038   − cmin 11376  -cneg 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379

This theorem is referenced by:  negeqi  11385  negeqd  11386  neg11  11444  renegcl  11456  negn0  11578  negf1o  11579  negfi  12103  infm3lem  12112  infm3  12113  riotaneg  12133  negiso  12134  infrenegsup  12137  elz  12502  elz2  12518  znegcl  12538  zindd  12605  zriotaneg  12617  ublbneg  12858  eqreznegel  12859  supminf  12860  zsupss  12862  qnegcl  12891  xnegeq  13134  ceilval  13770  expneg  14004  m1expcl2  14020  sqeqor  14151  sqrmo  15186  dvdsnegb  16212  lcmneg  16542  pcexp  16799  pcneg  16814  mulgneg2  19050  negfcncf  24885  xrhmeo  24912  evth2  24927  volsup2  25574  mbfi1fseqlem2  25685  mbfi1fseq  25690  lhop2  25988  lognegb  26567  lgsdir2lem4  27307  rpvmasum2  27491  ex-ceil  30535  elrgspnlem1  33336  hgt749d  34827  itgaddnclem2  37930  ftc1anclem5  37948  areacirc  37964  renegclALT  39339  rexzrexnn0  43161  dvdsrabdioph  43167  monotoddzzfi  43299  monotoddzz  43300  oddcomabszz  43301  infnsuprnmpt  45608  supminfrnmpt  45803  supminfxr  45822  etransclem17  46609  etransclem46  46638  etransclem47  46639  2zrngagrp  48609  digval  48958