Theorem negeq 9954

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

Syntax hints:   → wi 4   = wceq 1468  (class class class)co 6363  0cc0 9624   − cmin 9947  -cneg 9948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-rex 2797  df-rab 2800  df-v 3068  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-iota 5597  df-fv 5641  df-ov 6366  df-neg 9950

This theorem is referenced by:  negeqi  9955  negeqd  9956  neg11  10012  renegcl  10024  negn0  10136  negf1o  10137  negfi  10643  fiminre  10644  infm3lem  10656  infm3  10657  riotaneg  10675  negiso  10676  infrenegsup  10680  infmsupOLD  10681  infmrclOLD  10682  elz  11030  elz2  11045  znegcl  11063  zindd  11126  zriotaneg  11139  ublbneg  11339  eqreznegel  11340  supminf  11341  supminfOLD  11342  zsupss  11344  qnegcl  11372  xnegeq  11593  ceilval  12175  expneg  12394  m1expcl2  12408  sqeqor  12502  sqrmo  13475  dvdsnegb  14480  lcmneg  14730  pcexp  14971  pcneg  14985  mulgneg2  16945  negfcncf  22109  xrhmeo  22132  evth2  22146  volsup2  22723  mbfi1fseqlem2  22835  mbfi1fseq  22840  lhop2  23128  lognegb  23700  lgsdir2lem4  24415  rpvmasum2  24511  gxval  26149  gxnn0neg  26154  itgaddnclem2  32239  ftc1anclem5  32259  areacirc  32275  renegclALT  32768  rexzrexnn0  35887  dvdsrabdioph  35893  monotoddzzfi  36030  monotoddzz  36031  oddcomabszz  36032  etransclem17  38552  etransclem46  38581  etransclem47  38582  2zrngagrp  41133  digval  41598