Theorem negeq 8236

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

Syntax hints:   → wi 4   = wceq 1364  (class class class)co 5925  0cc0 7896   − cmin 8214  -cneg 8215

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3629  df-pr 3630  df-op 3632  df-uni 3841  df-br 4035  df-iota 5220  df-fv 5267  df-ov 5928  df-neg 8217

This theorem is referenced by:  negeqi  8237  negeqd  8238  neg11  8294  negf1o  8425  recexre  8622  negiso  8999  elz  9345  znegcl  9374  zaddcllemneg  9382  elz2  9414  zindd  9461  infrenegsupex  9685  supinfneg  9686  infsupneg  9687  supminfex  9688  ublbneg  9704  eqreznegel  9705  negm  9706  qnegcl  9727  xnegeq  9919  infssuzex  10340  infssuzcldc  10342  zsupssdc  10345  ceilqval  10415  exp3val  10650  expnegap0  10656  m1expcl2  10670  negfi  11410  dvdsnegb  11990  lcmneg  12267  pcexp  12503  pcneg  12519  znnen  12640  mulgneg2  13362  negcncf  14925  negfcncf  14926  lgsdir2lem4  15356  ex-ceil  15456