Theorem negeq 8168

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5891  0cc0 7829   − cmin 8146  -cneg 8147

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-rex 2474  df-v 2754  df-un 3148  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-iota 5193  df-fv 5239  df-ov 5894  df-neg 8149

This theorem is referenced by:  negeqi  8169  negeqd  8170  neg11  8226  negf1o  8357  recexre  8553  negiso  8930  elz  9273  znegcl  9302  zaddcllemneg  9310  elz2  9342  zindd  9389  infrenegsupex  9612  supinfneg  9613  infsupneg  9614  supminfex  9615  ublbneg  9631  eqreznegel  9632  negm  9633  qnegcl  9654  xnegeq  9845  ceilqval  10324  exp3val  10540  expnegap0  10546  m1expcl2  10560  negfi  11254  dvdsnegb  11833  infssuzex  11968  infssuzcldc  11970  zsupssdc  11973  lcmneg  12092  pcexp  12327  pcneg  12342  znnen  12417  mulgneg2  13062  negcncf  14485  negfcncf  14486  lgsdir2lem4  14829  ex-ceil  14875