Theorem negeq 10218

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

Syntax hints:   → wi 4   = wceq 1480  (class class class)co 6605  0cc0 9881   − cmin 10211  -cneg 10212

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-neg 10214

This theorem is referenced by:  negeqi  10219  negeqd  10220  neg11  10277  renegcl  10289  negn0  10404  negf1o  10405  negfi  10916  fiminre  10917  infm3lem  10926  infm3  10927  riotaneg  10947  negiso  10948  infrenegsup  10951  elz  11324  elz2  11339  znegcl  11357  zindd  11422  zriotaneg  11435  ublbneg  11717  eqreznegel  11718  supminf  11719  zsupss  11721  qnegcl  11749  xnegeq  11980  ceilval  12576  expneg  12805  m1expcl2  12819  sqeqor  12915  sqrmo  13921  dvdsnegb  14918  lcmneg  15235  pcexp  15483  pcneg  15497  mulgneg2  17491  negfcncf  22625  xrhmeo  22648  evth2  22662  volsup2  23274  mbfi1fseqlem2  23384  mbfi1fseq  23389  lhop2  23677  lognegb  24235  lgsdir2lem4  24948  rpvmasum2  25096  ex-ceil  27153  itgaddnclem2  33068  ftc1anclem5  33088  areacirc  33104  renegclALT  33696  rexzrexnn0  36815  dvdsrabdioph  36821  monotoddzzfi  36954  monotoddzz  36955  oddcomabszz  36956  infnsuprnmpt  38909  etransclem17  39743  etransclem46  39772  etransclem47  39773  2zrngagrp  41185  digval  41639