![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negeq | Structured version Visualization version GIF version |
Description: Equality theorem for negatives. (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
negeq | ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | oveq2 7427 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 11484 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 11484 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2790 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 (class class class)co 7419 0cc0 11145 − cmin 11481 -cneg 11482 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-dif 3947 df-un 3949 df-ss 3961 df-nul 4323 df-if 4531 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4910 df-br 5150 df-iota 6501 df-fv 6557 df-ov 7422 df-neg 11484 |
This theorem is referenced by: negeqi 11490 negeqd 11491 neg11 11548 renegcl 11560 negn0 11680 negf1o 11681 negfi 12201 infm3lem 12210 infm3 12211 riotaneg 12231 negiso 12232 infrenegsup 12235 elz 12598 elz2 12614 znegcl 12635 zindd 12701 zriotaneg 12713 ublbneg 12955 eqreznegel 12956 supminf 12957 zsupss 12959 qnegcl 12988 xnegeq 13226 ceilval 13844 expneg 14075 m1expcl2 14091 sqeqor 14220 sqrmo 15239 dvdsnegb 16259 lcmneg 16582 pcexp 16836 pcneg 16851 mulgneg2 19076 negfcncf 24893 xrhmeo 24920 evth2 24935 volsup2 25583 mbfi1fseqlem2 25695 mbfi1fseq 25700 lhop2 25997 lognegb 26574 lgsdir2lem4 27311 rpvmasum2 27495 ex-ceil 30335 hgt749d 34414 itgaddnclem2 37285 ftc1anclem5 37303 areacirc 37319 renegclALT 38567 rexzrexnn0 42368 dvdsrabdioph 42374 monotoddzzfi 42507 monotoddzz 42508 oddcomabszz 42509 infnsuprnmpt 44766 supminfrnmpt 44967 supminfxr 44986 etransclem17 45779 etransclem46 45808 etransclem47 45809 2zrngagrp 47499 digval 47859 |
Copyright terms: Public domain | W3C validator |