Theorem negeq 7445

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

Syntax hints:   → wi 4   = wceq 1285  (class class class)co 5565  0cc0 7120   − cmin 7423  -cneg 7424

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2613  df-un 2987  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-br 3807  df-iota 4918  df-fv 4961  df-ov 5568  df-neg 7426

This theorem is referenced by:  negeqi  7446  negeqd  7447  neg11  7503  negf1o  7630  recexre  7822  negiso  8177  elz  8511  znegcl  8540  zaddcllemneg  8548  elz2  8577  zindd  8623  infrenegsupex  8840  supinfneg  8841  infsupneg  8842  supminfex  8843  ublbneg  8856  eqreznegel  8857  negm  8858  qnegcl  8879  xnegeq  9047  ceilqval  9465  expival  9652  expnegap0  9658  m1expcl2  9672  negfi  10336  dvdsnegb  10445  infssuzex  10577  infssuzcldc  10579  lcmneg  10688  znnen  10843  ex-ceil  10849