Theorem negeq 11500

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7431  0cc0 11155   − cmin 11492  -cneg 11493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495

This theorem is referenced by:  negeqi  11501  negeqd  11502  neg11  11560  renegcl  11572  negn0  11692  negf1o  11693  negfi  12217  infm3lem  12226  infm3  12227  riotaneg  12247  negiso  12248  infrenegsup  12251  elz  12615  elz2  12631  znegcl  12652  zindd  12719  zriotaneg  12731  ublbneg  12975  eqreznegel  12976  supminf  12977  zsupss  12979  qnegcl  13008  xnegeq  13249  ceilval  13878  expneg  14110  m1expcl2  14126  sqeqor  14255  sqrmo  15290  dvdsnegb  16311  lcmneg  16640  pcexp  16897  pcneg  16912  mulgneg2  19126  negfcncf  24950  xrhmeo  24977  evth2  24992  volsup2  25640  mbfi1fseqlem2  25751  mbfi1fseq  25756  lhop2  26054  lognegb  26632  lgsdir2lem4  27372  rpvmasum2  27556  ex-ceil  30467  elrgspnlem1  33246  hgt749d  34664  itgaddnclem2  37686  ftc1anclem5  37704  areacirc  37720  renegclALT  38964  rexzrexnn0  42815  dvdsrabdioph  42821  monotoddzzfi  42954  monotoddzz  42955  oddcomabszz  42956  infnsuprnmpt  45257  supminfrnmpt  45456  supminfxr  45475  etransclem17  46266  etransclem46  46295  etransclem47  46296  2zrngagrp  48165  digval  48519