Theorem negeq 8482

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

Syntax hints:   → wi 4   = wceq 1398  (class class class)co 6058  0cc0 8143   − cmin 8460  -cneg 8461

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 3218  df-sn 3700  df-pr 3701  df-op 3703  df-uni 3920  df-br 4115  df-iota 5317  df-fv 5365  df-ov 6061  df-neg 8463

This theorem is referenced by:  negeqi  8483  negeqd  8484  neg11  8540  negf1o  8672  recexre  8869  negiso  9246  elz  9596  znegcl  9625  zaddcllemneg  9633  elz2  9666  zindd  9714  infrenegsupex  9944  supinfneg  9945  infsupneg  9946  supminfex  9947  ublbneg  9963  eqreznegel  9964  negm  9965  qnegcl  9986  xnegeq  10179  infssuzex  10615  infssuzcldc  10617  zsupssdc  10622  ceilqval  10692  exp3val  10927  expnegap0  10933  m1expcl2  10947  negfi  11938  dvdsnegb  12519  lcmneg  12796  pcexp  13032  pcneg  13048  znnen  13233  mulgneg2  13909  negcncf  15596  negfcncf  15597  lgsdir2lem4  16030  ex-ceil  16620