![]() |
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 5698 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 7753 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 7753 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2152 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1296 (class class class)co 5690 0cc0 7447 − cmin 7750 -cneg 7751 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 |
This theorem depends on definitions: df-bi 116 df-3an 929 df-tru 1299 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-rex 2376 df-v 2635 df-un 3017 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-br 3868 df-iota 5014 df-fv 5057 df-ov 5693 df-neg 7753 |
This theorem is referenced by: negeqi 7773 negeqd 7774 neg11 7830 negf1o 7957 recexre 8152 negiso 8513 elz 8850 znegcl 8879 zaddcllemneg 8887 elz2 8916 zindd 8963 infrenegsupex 9181 supinfneg 9182 infsupneg 9183 supminfex 9184 ublbneg 9197 eqreznegel 9198 negm 9199 qnegcl 9220 xnegeq 9393 ceilqval 9862 exp3val 10072 expnegap0 10078 m1expcl2 10092 negfi 10774 dvdsnegb 11240 infssuzex 11372 infssuzcldc 11374 lcmneg 11483 znnen 11638 negcncf 12353 negfcncf 12354 ex-ceil 12370 |
Copyright terms: Public domain | W3C validator |