Theorem negeq 10152

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

Syntax hints:   → wi 4   = wceq 1475  (class class class)co 6549  0cc0 9815   − cmin 10145  -cneg 10146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148

This theorem is referenced by:  negeqi  10153  negeqd  10154  neg11  10211  renegcl  10223  negn0  10338  negf1o  10339  negfi  10850  fiminre  10851  infm3lem  10860  infm3  10861  riotaneg  10879  negiso  10880  infrenegsup  10883  elz  11256  elz2  11271  znegcl  11289  zindd  11354  zriotaneg  11367  ublbneg  11649  eqreznegel  11650  supminf  11651  zsupss  11653  qnegcl  11681  xnegeq  11912  ceilval  12501  expneg  12730  m1expcl2  12744  sqeqor  12840  sqrmo  13840  dvdsnegb  14837  lcmneg  15154  pcexp  15402  pcneg  15416  mulgneg2  17398  negfcncf  22530  xrhmeo  22553  evth2  22567  volsup2  23179  mbfi1fseqlem2  23289  mbfi1fseq  23294  lhop2  23582  lognegb  24140  lgsdir2lem4  24853  rpvmasum2  25001  ex-ceil  26697  itgaddnclem2  32639  ftc1anclem5  32659  areacirc  32675  renegclALT  33267  rexzrexnn0  36386  dvdsrabdioph  36392  monotoddzzfi  36525  monotoddzz  36526  oddcomabszz  36527  etransclem17  39144  etransclem46  39173  etransclem47  39174  2zrngagrp  41733  digval  42190