Theorem negeq 11588

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7451  0cc0 11239   − cmin 11580   -cneg 11581

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-iota 6520  df-fv 6574  df-ov 7454  df-neg 11583

This theorem is used by:  negeqi  11589  negeqd  11590  neg11  11648  renegcl  11660  negn0  11784  negf1o  11785  negfi  12306  infm3lem  12315  infm3  12316  riotaneg  12336  negiso  12337  infrenegsup  12340  elz  12735  elz2  12751  znegcl  12771  zindd  12840  zriotaneg  12852  ublbneg  13100  eqreznegel  13101  supminf  13102  zsupss  13104  qnegcl  13134  xnegeq  13377  ceilval  14018  expneg  14252  m1expcl2  14268  sqeqor  14401  sqrmo  15461  dvdsnegb  16487  lcmneg  16822  pcexp  17081  pcneg  17096  mulgneg2  19368  negfcncf  25299  xrhmeo  25322  evth2  25336  volsup2  25981  mbfi1fseqlem2  26092  mbfi1fseq  26097  lhop2  26390  lognegb  26975  lgsdir2lem4  27712  rpvmasum2  27896  ex-ceil  31106  elrgspnlem1  33902  hgt749d  35389  itgaddnclem2  38865  ftc1anclem5  38883  areacirc  38899  renegclALT  40286  rexzrexnn0  44077  dvdsrabdioph  44083  monotoddzzfi  44215  monotoddzz  44216  oddcomabszz  44217  infnsuprnmpt  46535  supminfrnmpt  46728  supminfxr  46747  etransclem17  47534  etransclem46  47563  etransclem47  47564  2zrngagrp  49619  laznegcl  49736  digval  50041