Theorem negeq 11474

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7414  0cc0 11125   − cmin 11466  -cneg 11467

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6489  df-fv 6541  df-ov 7417  df-neg 11469

This theorem is used by:  negeqi  11475  negeqd  11476  neg11  11534  renegcl  11546  negn0  11668  negf1o  11669  negfi  12189  infm3lem  12198  infm3  12199  riotaneg  12219  negiso  12220  infrenegsup  12223  elz  12618  elz2  12634  znegcl  12654  zindd  12723  zriotaneg  12735  ublbneg  12983  eqreznegel  12984  supminf  12985  zsupss  12987  qnegcl  13017  xnegeq  13260  ceilval  13900  expneg  14134  m1expcl2  14150  sqeqor  14281  sqrmo  15339  dvdsnegb  16364  lcmneg  16694  pcexp  16952  pcneg  16967  mulgneg2  19232  negfcncf  25152  xrhmeo  25175  evth2  25189  volsup2  25834  mbfi1fseqlem2  25945  mbfi1fseq  25950  lhop2  26243  lognegb  26828  lgsdir2lem4  27565  rpvmasum2  27749  ex-ceil  30929  elrgspnlem1  33683  hgt749d  35158  itgaddnclem2  38429  ftc1anclem5  38447  areacirc  38463  renegclALT  39837  rexzrexnn0  43646  dvdsrabdioph  43652  monotoddzzfi  43784  monotoddzz  43785  oddcomabszz  43786  infnsuprnmpt  46080  supminfrnmpt  46274  supminfxr  46293  etransclem17  47080  etransclem46  47109  etransclem47  47110  2zrngagrp  49165  digval  49529