ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  negeq Unicode version

Theorem negeq 7978
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
StepHypRef Expression
1 oveq2 5789 . 2  |-  ( A  =  B  ->  (
0  -  A )  =  ( 0  -  B ) )
2 df-neg 7959 . 2  |-  -u A  =  ( 0  -  A )
3 df-neg 7959 . 2  |-  -u B  =  ( 0  -  B )
41, 2, 33eqtr4g 2198 1  |-  ( A  =  B  ->  -u A  =  -u B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1332  (class class class)co 5781   0cc0 7643    - cmin 7956   -ucneg 7957
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-rex 2423  df-v 2691  df-un 3079  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-br 3937  df-iota 5095  df-fv 5138  df-ov 5784  df-neg 7959
This theorem is referenced by:  negeqi  7979  negeqd  7980  neg11  8036  negf1o  8167  recexre  8363  negiso  8736  elz  9079  znegcl  9108  zaddcllemneg  9116  elz2  9145  zindd  9192  infrenegsupex  9415  supinfneg  9416  infsupneg  9417  supminfex  9418  ublbneg  9431  eqreznegel  9432  negm  9433  qnegcl  9454  xnegeq  9639  ceilqval  10109  exp3val  10325  expnegap0  10331  m1expcl2  10345  negfi  11030  dvdsnegb  11544  infssuzex  11676  infssuzcldc  11678  lcmneg  11789  znnen  11945  negcncf  12794  negfcncf  12795  ex-ceil  13107
  Copyright terms: Public domain W3C validator