Theorem negeq 11413

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

Syntax hints:   → wi 4   = wceq 1540  (class class class)co 7387  0cc0 11068   − cmin 11405  -cneg 11406

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-iota 6464  df-fv 6519  df-ov 7390  df-neg 11408

This theorem is referenced by:  negeqi  11414  negeqd  11415  neg11  11473  renegcl  11485  negn0  11607  negf1o  11608  negfi  12132  infm3lem  12141  infm3  12142  riotaneg  12162  negiso  12163  infrenegsup  12166  elz  12531  elz2  12547  znegcl  12568  zindd  12635  zriotaneg  12647  ublbneg  12892  eqreznegel  12893  supminf  12894  zsupss  12896  qnegcl  12925  xnegeq  13167  ceilval  13800  expneg  14034  m1expcl2  14050  sqeqor  14181  sqrmo  15217  dvdsnegb  16243  lcmneg  16573  pcexp  16830  pcneg  16845  mulgneg2  19040  negfcncf  24817  xrhmeo  24844  evth2  24859  volsup2  25506  mbfi1fseqlem2  25617  mbfi1fseq  25622  lhop2  25920  lognegb  26499  lgsdir2lem4  27239  rpvmasum2  27423  ex-ceil  30377  elrgspnlem1  33193  hgt749d  34640  itgaddnclem2  37673  ftc1anclem5  37691  areacirc  37707  renegclALT  38956  rexzrexnn0  42792  dvdsrabdioph  42798  monotoddzzfi  42931  monotoddzz  42932  oddcomabszz  42933  infnsuprnmpt  45244  supminfrnmpt  45441  supminfxr  45460  etransclem17  46249  etransclem46  46278  etransclem47  46279  2zrngagrp  48237  digval  48587