Theorem negeq 8371

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

Syntax hints:   → wi 4   = wceq 1397  (class class class)co 6017  0cc0 8031   − cmin 8349  -cneg 8350

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-rex 2516  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-br 4089  df-iota 5286  df-fv 5334  df-ov 6020  df-neg 8352

This theorem is referenced by:  negeqi  8372  negeqd  8373  neg11  8429  negf1o  8560  recexre  8757  negiso  9134  elz  9480  znegcl  9509  zaddcllemneg  9517  elz2  9550  zindd  9597  infrenegsupex  9827  supinfneg  9828  infsupneg  9829  supminfex  9830  ublbneg  9846  eqreznegel  9847  negm  9848  qnegcl  9869  xnegeq  10061  infssuzex  10492  infssuzcldc  10494  zsupssdc  10497  ceilqval  10567  exp3val  10802  expnegap0  10808  m1expcl2  10822  negfi  11788  dvdsnegb  12368  lcmneg  12645  pcexp  12881  pcneg  12897  znnen  13018  mulgneg2  13742  negcncf  15328  negfcncf  15329  lgsdir2lem4  15759  ex-ceil  16322