Theorem negeq 11474

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7405  0cc0 11129   − cmin 11466  -cneg 11467

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 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-iota 6484  df-fv 6539  df-ov 7408  df-neg 11469

This theorem is referenced by:  negeqi  11475  negeqd  11476  neg11  11534  renegcl  11546  negn0  11666  negf1o  11667  negfi  12191  infm3lem  12200  infm3  12201  riotaneg  12221  negiso  12222  infrenegsup  12225  elz  12590  elz2  12606  znegcl  12627  zindd  12694  zriotaneg  12706  ublbneg  12949  eqreznegel  12950  supminf  12951  zsupss  12953  qnegcl  12982  xnegeq  13223  ceilval  13855  expneg  14087  m1expcl2  14103  sqeqor  14234  sqrmo  15270  dvdsnegb  16293  lcmneg  16622  pcexp  16879  pcneg  16894  mulgneg2  19091  negfcncf  24868  xrhmeo  24895  evth2  24910  volsup2  25558  mbfi1fseqlem2  25669  mbfi1fseq  25674  lhop2  25972  lognegb  26551  lgsdir2lem4  27291  rpvmasum2  27475  ex-ceil  30429  elrgspnlem1  33237  hgt749d  34681  itgaddnclem2  37703  ftc1anclem5  37721  areacirc  37737  renegclALT  38981  rexzrexnn0  42827  dvdsrabdioph  42833  monotoddzzfi  42966  monotoddzz  42967  oddcomabszz  42968  infnsuprnmpt  45274  supminfrnmpt  45472  supminfxr  45491  etransclem17  46280  etransclem46  46309  etransclem47  46310  2zrngagrp  48224  digval  48578