Theorem negeq 10614

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

Syntax hints:   → wi 4   = wceq 1601  (class class class)co 6922  0cc0 10272   − cmin 10606  -cneg 10607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-rex 3096  df-rab 3099  df-v 3400  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-nul 4142  df-if 4308  df-sn 4399  df-pr 4401  df-op 4405  df-uni 4672  df-br 4887  df-iota 6099  df-fv 6143  df-ov 6925  df-neg 10609

This theorem is referenced by:  negeqi  10615  negeqd  10616  neg11  10674  renegcl  10686  negn0  10804  negf1o  10805  negfi  11325  fiminre  11326  infm3lem  11335  infm3  11336  riotaneg  11356  negiso  11357  infrenegsup  11360  elz  11730  elz2  11745  znegcl  11764  zindd  11830  zriotaneg  11843  ublbneg  12080  eqreznegel  12081  supminf  12082  zsupss  12084  qnegcl  12113  xnegeq  12350  ceilval  12958  expneg  13186  m1expcl2  13200  sqeqor  13297  sqrmo  14399  dvdsnegb  15406  lcmneg  15722  pcexp  15968  pcneg  15982  mulgneg2  17960  negfcncf  23130  xrhmeo  23153  evth2  23167  volsup2  23809  mbfi1fseqlem2  23920  mbfi1fseq  23925  lhop2  24215  lognegb  24773  lgsdir2lem4  25505  rpvmasum2  25653  ex-ceil  27880  hgt749d  31329  itgaddnclem2  34094  ftc1anclem5  34114  areacirc  34130  renegclALT  35117  rexzrexnn0  38328  dvdsrabdioph  38334  monotoddzzfi  38466  monotoddzz  38467  oddcomabszz  38468  infnsuprnmpt  40376  supminfrnmpt  40578  supminfxr  40599  etransclem17  41395  etransclem46  41424  etransclem47  41425  2zrngagrp  42958  digval  43407