Theorem negeq 7404

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 5572	. 2 |- ( A = B -> ( 0 - A ) = ( 0 - B ) )
2		df-neg 7385	. 2 |- -u A = ( 0 - A )
3		df-neg 7385	. 2 |- -u B = ( 0 - B )
4	1, 2, 3	3eqtr4g 2140	1 |- ( A = B -> -u A = -u B )

Syntax hints:   -> wi 4   = wceq 1285  (class class class)co 5564   0cc0 7079   - cmin 7382   -ucneg 7383

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-rex 2359  df-v 2612  df-un 2987  df-sn 3423  df-pr 3424  df-op 3426  df-uni 3623  df-br 3807  df-iota 4918  df-fv 4961  df-ov 5567  df-neg 7385

This theorem is referenced by:  negeqi  7405  negeqd  7406  neg11  7462  negf1o  7589  recexre  7781  negiso  8136  elz  8470  znegcl  8499  zaddcllemneg  8507  elz2  8536  zindd  8582  infrenegsupex  8799  supinfneg  8800  infsupneg  8801  supminfex  8802  ublbneg  8815  eqreznegel  8816  negm  8817  qnegcl  8838  xnegeq  9006  ceilqval  9424  expival  9611  expnegap0  9617  m1expcl2  9631  negfi  10295  dvdsnegb  10404  infssuzex  10536  infssuzcldc  10538  lcmneg  10647  znnen  10802  ex-ceil  10808