Theorem negeq 11420

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7390  0cc0 11075   − cmin 11412  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415

This theorem is referenced by:  negeqi  11421  negeqd  11422  neg11  11480  renegcl  11492  negn0  11614  negf1o  11615  negfi  12139  infm3lem  12148  infm3  12149  riotaneg  12169  negiso  12170  infrenegsup  12173  elz  12538  elz2  12554  znegcl  12575  zindd  12642  zriotaneg  12654  ublbneg  12899  eqreznegel  12900  supminf  12901  zsupss  12903  qnegcl  12932  xnegeq  13174  ceilval  13807  expneg  14041  m1expcl2  14057  sqeqor  14188  sqrmo  15224  dvdsnegb  16250  lcmneg  16580  pcexp  16837  pcneg  16852  mulgneg2  19047  negfcncf  24824  xrhmeo  24851  evth2  24866  volsup2  25513  mbfi1fseqlem2  25624  mbfi1fseq  25629  lhop2  25927  lognegb  26506  lgsdir2lem4  27246  rpvmasum2  27430  ex-ceil  30384  elrgspnlem1  33200  hgt749d  34647  itgaddnclem2  37680  ftc1anclem5  37698  areacirc  37714  renegclALT  38963  rexzrexnn0  42799  dvdsrabdioph  42805  monotoddzzfi  42938  monotoddzz  42939  oddcomabszz  42940  infnsuprnmpt  45251  supminfrnmpt  45448  supminfxr  45467  etransclem17  46256  etransclem46  46285  etransclem47  46286  2zrngagrp  48241  digval  48591