Theorem negeq 8099

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

Syntax hints:   → wi 4   = wceq 1348  (class class class)co 5850  0cc0 7761   − cmin 8077  -cneg 8078

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-rex 2454  df-v 2732  df-un 3125  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-br 3988  df-iota 5158  df-fv 5204  df-ov 5853  df-neg 8080

This theorem is referenced by:  negeqi  8100  negeqd  8101  neg11  8157  negf1o  8288  recexre  8484  negiso  8858  elz  9201  znegcl  9230  zaddcllemneg  9238  elz2  9270  zindd  9317  infrenegsupex  9540  supinfneg  9541  infsupneg  9542  supminfex  9543  ublbneg  9559  eqreznegel  9560  negm  9561  qnegcl  9582  xnegeq  9771  ceilqval  10249  exp3val  10465  expnegap0  10471  m1expcl2  10485  negfi  11178  dvdsnegb  11757  infssuzex  11891  infssuzcldc  11893  zsupssdc  11896  lcmneg  12015  pcexp  12250  pcneg  12265  znnen  12340  negcncf  13303  negfcncf  13304  lgsdir2lem4  13647  ex-ceil  13682