Theorem negeq 8468

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6052  0cc0 8129   − cmin 8446  -cneg 8447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-rex 2528  df-v 2817  df-un 3217  df-sn 3697  df-pr 3698  df-op 3700  df-uni 3917  df-br 4112  df-iota 5314  df-fv 5362  df-ov 6055  df-neg 8449

This theorem is referenced by:  negeqi  8469  negeqd  8470  neg11  8526  negf1o  8657  recexre  8854  negiso  9231  elz  9581  znegcl  9610  zaddcllemneg  9618  elz2  9651  zindd  9699  infrenegsupex  9929  supinfneg  9930  infsupneg  9931  supminfex  9932  ublbneg  9948  eqreznegel  9949  negm  9950  qnegcl  9971  xnegeq  10163  infssuzex  10597  infssuzcldc  10599  zsupssdc  10602  ceilqval  10672  exp3val  10907  expnegap0  10913  m1expcl2  10927  negfi  11917  dvdsnegb  12498  lcmneg  12775  pcexp  13011  pcneg  13027  znnen  13166  mulgneg2  13890  negcncf  15487  negfcncf  15488  lgsdir2lem4  15921  ex-ceil  16511