Theorem negeq 11466

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7419  0cc0 11117   − cmin 11458  -cneg 11459

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-neg 11461

This theorem is used by:  negeqi  11467  negeqd  11468  neg11  11526  renegcl  11538  negn0  11660  negf1o  11661  negfi  12181  infm3lem  12190  infm3  12191  riotaneg  12211  negiso  12212  infrenegsup  12215  elz  12610  elz2  12626  znegcl  12646  zindd  12715  zriotaneg  12727  ublbneg  12975  eqreznegel  12976  supminf  12977  zsupss  12979  qnegcl  13008  xnegeq  13251  ceilval  13891  expneg  14125  m1expcl2  14141  sqeqor  14272  sqrmo  15328  dvdsnegb  16355  lcmneg  16685  pcexp  16943  pcneg  16958  mulgneg2  19220  negfcncf  25135  xrhmeo  25158  evth2  25172  volsup2  25817  mbfi1fseqlem2  25928  mbfi1fseq  25933  lhop2  26227  lognegb  26808  lgsdir2lem4  27545  rpvmasum2  27729  ex-ceil  30872  elrgspnlem1  33628  hgt749d  35103  itgaddnclem2  38389  ftc1anclem5  38407  areacirc  38423  renegclALT  39797  rexzrexnn0  43591  dvdsrabdioph  43597  monotoddzzfi  43729  monotoddzz  43730  oddcomabszz  43731  infnsuprnmpt  46025  supminfrnmpt  46219  supminfxr  46238  etransclem17  47025  etransclem46  47054  etransclem47  47055  2zrngagrp  49073  digval  49437