Theorem negeq 11196

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

Syntax hints:   → wi 4   = wceq 1541  (class class class)co 7268  0cc0 10855   − cmin 11188  -cneg 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-iota 6388  df-fv 6438  df-ov 7271  df-neg 11191

This theorem is referenced by:  negeqi  11197  negeqd  11198  neg11  11255  renegcl  11267  negn0  11387  negf1o  11388  negfi  11907  infm3lem  11916  infm3  11917  riotaneg  11937  negiso  11938  infrenegsup  11941  elz  12304  elz2  12320  znegcl  12338  zindd  12404  zriotaneg  12417  ublbneg  12655  eqreznegel  12656  supminf  12657  zsupss  12659  qnegcl  12688  xnegeq  12923  ceilval  13539  expneg  13771  m1expcl2  13785  sqeqor  13913  sqrmo  14944  dvdsnegb  15964  lcmneg  16289  pcexp  16541  pcneg  16556  mulgneg2  18718  negfcncf  24067  xrhmeo  24090  evth2  24104  volsup2  24750  mbfi1fseqlem2  24862  mbfi1fseq  24867  lhop2  25160  lognegb  25726  lgsdir2lem4  26457  rpvmasum2  26641  ex-ceil  28791  hgt749d  32608  itgaddnclem2  35815  ftc1anclem5  35833  areacirc  35849  renegclALT  36956  rexzrexnn0  40606  dvdsrabdioph  40612  monotoddzzfi  40744  monotoddzz  40745  oddcomabszz  40746  infnsuprnmpt  42749  supminfrnmpt  42939  supminfxr  42958  etransclem17  43746  etransclem46  43775  etransclem47  43776  2zrngagrp  45453  digval  45896