Theorem negeq 10273

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

Syntax hints:   → wi 4   = wceq 1483  (class class class)co 6650  0cc0 9936   − cmin 10266  -cneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269

This theorem is referenced by:  negeqi  10274  negeqd  10275  neg11  10332  renegcl  10344  negn0  10459  negf1o  10460  negfi  10971  fiminre  10972  infm3lem  10981  infm3  10982  riotaneg  11002  negiso  11003  infrenegsup  11006  elz  11379  elz2  11394  znegcl  11412  zindd  11478  zriotaneg  11491  ublbneg  11773  eqreznegel  11774  supminf  11775  zsupss  11777  qnegcl  11805  xnegeq  12038  ceilval  12639  expneg  12868  m1expcl2  12882  sqeqor  12978  sqrmo  13992  dvdsnegb  14999  lcmneg  15316  pcexp  15564  pcneg  15578  mulgneg2  17575  negfcncf  22722  xrhmeo  22745  evth2  22759  volsup2  23373  mbfi1fseqlem2  23483  mbfi1fseq  23488  lhop2  23778  lognegb  24336  lgsdir2lem4  25053  rpvmasum2  25201  ex-ceil  27305  hgt749d  30727  itgaddnclem2  33469  ftc1anclem5  33489  areacirc  33505  renegclALT  34249  rexzrexnn0  37368  dvdsrabdioph  37374  monotoddzzfi  37507  monotoddzz  37508  oddcomabszz  37509  infnsuprnmpt  39465  supminfrnmpt  39672  supminfxr  39694  etransclem17  40468  etransclem46  40497  etransclem47  40498  2zrngagrp  41943  digval  42392