Theorem negeq 11556

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  (class class class)co 7424  0cc0 11207   − cmin 11548   -cneg 11549

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-iota 6497  df-fv 6551  df-ov 7427  df-neg 11551

This theorem is used by:  negeqi  11557  negeqd  11558  neg11  11616  renegcl  11628  negn0  11752  negf1o  11753  negfi  12273  infm3lem  12282  infm3  12283  riotaneg  12303  negiso  12304  infrenegsup  12307  elz  12702  elz2  12718  znegcl  12738  zindd  12807  zriotaneg  12819  ublbneg  13067  eqreznegel  13068  supminf  13069  zsupss  13071  qnegcl  13101  xnegeq  13344  ceilval  13985  expneg  14219  m1expcl2  14235  sqeqor  14367  sqrmo  15427  dvdsnegb  16452  lcmneg  16787  pcexp  17046  pcneg  17061  mulgneg2  19327  negfcncf  25253  xrhmeo  25276  evth2  25290  volsup2  25935  mbfi1fseqlem2  26046  mbfi1fseq  26051  lhop2  26344  lognegb  26927  lgsdir2lem4  27664  rpvmasum2  27848  ex-ceil  31058  elrgspnlem1  33853  hgt749d  35328  itgaddnclem2  38734  ftc1anclem5  38752  areacirc  38768  renegclALT  40157  rexzrexnn0  43948  dvdsrabdioph  43954  monotoddzzfi  44086  monotoddzz  44087  oddcomabszz  44088  infnsuprnmpt  46398  supminfrnmpt  46591  supminfxr  46610  etransclem17  47397  etransclem46  47426  etransclem47  47427  2zrngagrp  49482  digval  49846