Theorem negeq 11549

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  (class class class)co 7420  0cc0 11200   − cmin 11541  -cneg 11542

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 6494  df-fv 6546  df-ov 7423  df-neg 11544

This theorem is used by:  negeqi  11550  negeqd  11551  neg11  11609  renegcl  11621  negn0  11745  negf1o  11746  negfi  12266  infm3lem  12275  infm3  12276  riotaneg  12296  negiso  12297  infrenegsup  12300  elz  12695  elz2  12711  znegcl  12731  zindd  12800  zriotaneg  12812  ublbneg  13060  eqreznegel  13061  supminf  13062  zsupss  13064  qnegcl  13094  xnegeq  13337  ceilval  13978  expneg  14212  m1expcl2  14228  sqeqor  14360  sqrmo  15418  dvdsnegb  16443  lcmneg  16778  pcexp  17037  pcneg  17052  mulgneg2  19318  negfcncf  25244  xrhmeo  25267  evth2  25281  volsup2  25926  mbfi1fseqlem2  26037  mbfi1fseq  26042  lhop2  26335  lognegb  26918  lgsdir2lem4  27655  rpvmasum2  27839  ex-ceil  31049  elrgspnlem1  33803  hgt749d  35278  itgaddnclem2  38597  ftc1anclem5  38615  areacirc  38631  renegclALT  40020  rexzrexnn0  43810  dvdsrabdioph  43816  monotoddzzfi  43948  monotoddzz  43949  oddcomabszz  43950  infnsuprnmpt  46261  supminfrnmpt  46454  supminfxr  46473  etransclem17  47260  etransclem46  47289  etransclem47  47290  2zrngagrp  49345  digval  49709