Theorem negeq 11201

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

Syntax hints:   → wi 4   = wceq 1539  (class class class)co 7268  0cc0 10859   − cmin 11193  -cneg 11194

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3432  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5075  df-iota 6385  df-fv 6435  df-ov 7271  df-neg 11196

This theorem is referenced by:  negeqi  11202  negeqd  11203  neg11  11260  renegcl  11272  negn0  11392  negf1o  11393  negfi  11912  infm3lem  11921  infm3  11922  riotaneg  11942  negiso  11943  infrenegsup  11946  elz  12309  elz2  12325  znegcl  12343  zindd  12409  zriotaneg  12423  ublbneg  12661  eqreznegel  12662  supminf  12663  zsupss  12665  qnegcl  12694  xnegeq  12929  ceilval  13546  expneg  13778  m1expcl2  13792  sqeqor  13920  sqrmo  14951  dvdsnegb  15971  lcmneg  16296  pcexp  16548  pcneg  16563  mulgneg2  18725  negfcncf  24074  xrhmeo  24097  evth2  24111  volsup2  24757  mbfi1fseqlem2  24869  mbfi1fseq  24874  lhop2  25167  lognegb  25733  lgsdir2lem4  26464  rpvmasum2  26648  ex-ceil  28798  hgt749d  32615  itgaddnclem2  35822  ftc1anclem5  35840  areacirc  35856  renegclALT  36963  rexzrexnn0  40612  dvdsrabdioph  40618  monotoddzzfi  40750  monotoddzz  40751  oddcomabszz  40752  infnsuprnmpt  42755  supminfrnmpt  42944  supminfxr  42963  etransclem17  43751  etransclem46  43780  etransclem47  43781  2zrngagrp  45457  digval  45900