![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > negeq | GIF version |
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
negeq | ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 5573 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 7426 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 7426 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2140 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1285 (class class class)co 5565 0cc0 7120 − cmin 7423 -cneg 7424 |
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 2613 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 5568 df-neg 7426 |
This theorem is referenced by: negeqi 7446 negeqd 7447 neg11 7503 negf1o 7630 recexre 7822 negiso 8177 elz 8511 znegcl 8540 zaddcllemneg 8548 elz2 8577 zindd 8623 infrenegsupex 8840 supinfneg 8841 infsupneg 8842 supminfex 8843 ublbneg 8856 eqreznegel 8857 negm 8858 qnegcl 8879 xnegeq 9047 ceilqval 9465 expival 9652 expnegap0 9658 m1expcl2 9672 negfi 10336 dvdsnegb 10445 infssuzex 10577 infssuzcldc 10579 lcmneg 10688 znnen 10843 ex-ceil 10849 |
Copyright terms: Public domain | W3C validator |