Theorem negeq 8219

Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.)

Assertion

Ref	Expression
negeq	|- ( A = B -> -u A = -u B )

Proof of Theorem negeq

Step	Hyp	Ref	Expression
1		oveq2 5930	. 2 |- ( A = B -> ( 0 - A ) = ( 0 - B ) )
2		df-neg 8200	. 2 |- -u A = ( 0 - A )
3		df-neg 8200	. 2 |- -u B = ( 0 - B )
4	1, 2, 3	3eqtr4g 2254	1 |- ( A = B -> -u A = -u B )

Syntax hints:   -> wi 4   = wceq 1364  (class class class)co 5922   0cc0 7879   - cmin 8197   -ucneg 8198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-rex 2481  df-v 2765  df-un 3161  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-br 4034  df-iota 5219  df-fv 5266  df-ov 5925  df-neg 8200

This theorem is referenced by:  negeqi  8220  negeqd  8221  neg11  8277  negf1o  8408  recexre  8605  negiso  8982  elz  9328  znegcl  9357  zaddcllemneg  9365  elz2  9397  zindd  9444  infrenegsupex  9668  supinfneg  9669  infsupneg  9670  supminfex  9671  ublbneg  9687  eqreznegel  9688  negm  9689  qnegcl  9710  xnegeq  9902  infssuzex  10323  infssuzcldc  10325  zsupssdc  10328  ceilqval  10398  exp3val  10633  expnegap0  10639  m1expcl2  10653  negfi  11393  dvdsnegb  11973  lcmneg  12242  pcexp  12478  pcneg  12494  znnen  12615  mulgneg2  13286  negcncf  14841  negfcncf  14842  lgsdir2lem4  15272  ex-ceil  15372