Theorem negeq 11528

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

Syntax hints:   → wi 4   = wceq 1537  (class class class)co 7448  0cc0 11184   − cmin 11520  -cneg 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523

This theorem is referenced by:  negeqi  11529  negeqd  11530  neg11  11587  renegcl  11599  negn0  11719  negf1o  11720  negfi  12244  infm3lem  12253  infm3  12254  riotaneg  12274  negiso  12275  infrenegsup  12278  elz  12641  elz2  12657  znegcl  12678  zindd  12744  zriotaneg  12756  ublbneg  12998  eqreznegel  12999  supminf  13000  zsupss  13002  qnegcl  13031  xnegeq  13269  ceilval  13889  expneg  14120  m1expcl2  14136  sqeqor  14265  sqrmo  15300  dvdsnegb  16322  lcmneg  16650  pcexp  16906  pcneg  16921  mulgneg2  19148  negfcncf  24969  xrhmeo  24996  evth2  25011  volsup2  25659  mbfi1fseqlem2  25771  mbfi1fseq  25776  lhop2  26074  lognegb  26650  lgsdir2lem4  27390  rpvmasum2  27574  ex-ceil  30480  hgt749d  34626  itgaddnclem2  37639  ftc1anclem5  37657  areacirc  37673  renegclALT  38919  rexzrexnn0  42760  dvdsrabdioph  42766  monotoddzzfi  42899  monotoddzz  42900  oddcomabszz  42901  infnsuprnmpt  45159  supminfrnmpt  45360  supminfxr  45379  etransclem17  46172  etransclem46  46201  etransclem47  46202  2zrngagrp  47972  digval  48332