Theorem negeq 10311

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

Syntax hints:   → wi 4   = wceq 1523  (class class class)co 6690  0cc0 9974   − cmin 10304  -cneg 10305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307

This theorem is referenced by:  negeqi  10312  negeqd  10313  neg11  10370  renegcl  10382  negn0  10497  negf1o  10498  negfi  11009  fiminre  11010  infm3lem  11019  infm3  11020  riotaneg  11040  negiso  11041  infrenegsup  11044  elz  11417  elz2  11432  znegcl  11450  zindd  11516  zriotaneg  11529  ublbneg  11811  eqreznegel  11812  supminf  11813  zsupss  11815  qnegcl  11843  xnegeq  12076  ceilval  12679  expneg  12908  m1expcl2  12922  sqeqor  13018  sqrmo  14036  dvdsnegb  15046  lcmneg  15363  pcexp  15611  pcneg  15625  mulgneg2  17622  negfcncf  22769  xrhmeo  22792  evth2  22806  volsup2  23419  mbfi1fseqlem2  23528  mbfi1fseq  23533  lhop2  23823  lognegb  24381  lgsdir2lem4  25098  rpvmasum2  25246  ex-ceil  27435  hgt749d  30855  itgaddnclem2  33599  ftc1anclem5  33619  areacirc  33635  renegclALT  34567  rexzrexnn0  37685  dvdsrabdioph  37691  monotoddzzfi  37824  monotoddzz  37825  oddcomabszz  37826  infnsuprnmpt  39779  supminfrnmpt  39985  supminfxr  40007  etransclem17  40786  etransclem46  40815  etransclem47  40816  2zrngagrp  42268  digval  42717