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 7153 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 10861 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 10861 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 (class class class)co 7145 0cc0 10525 − cmin 10858 -cneg 10859 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rex 3141 df-rab 3144 df-v 3494 df-dif 3936 df-un 3938 df-in 3940 df-ss 3949 df-nul 4289 df-if 4464 df-sn 4558 df-pr 4560 df-op 4564 df-uni 4831 df-br 5058 df-iota 6307 df-fv 6356 df-ov 7148 df-neg 10861 |
This theorem is referenced by: negeqi 10867 negeqd 10868 neg11 10925 renegcl 10937 negn0 11057 negf1o 11058 negfi 11577 fiminreOLD 11578 infm3lem 11587 infm3 11588 riotaneg 11608 negiso 11609 infrenegsup 11612 elz 11971 elz2 11987 znegcl 12005 zindd 12071 zriotaneg 12084 ublbneg 12321 eqreznegel 12322 supminf 12323 zsupss 12325 qnegcl 12353 xnegeq 12588 ceilval 13196 expneg 13425 m1expcl2 13439 sqeqor 13566 sqrmo 14599 dvdsnegb 15615 lcmneg 15935 pcexp 16184 pcneg 16198 mulgneg2 18199 negfcncf 23454 xrhmeo 23477 evth2 23491 volsup2 24133 mbfi1fseqlem2 24244 mbfi1fseq 24249 lhop2 24539 lognegb 25100 lgsdir2lem4 25831 rpvmasum2 26015 ex-ceil 28154 hgt749d 31819 itgaddnclem2 34832 ftc1anclem5 34852 areacirc 34868 renegclALT 35979 rexzrexnn0 39279 dvdsrabdioph 39285 monotoddzzfi 39417 monotoddzz 39418 oddcomabszz 39419 infnsuprnmpt 41398 supminfrnmpt 41595 supminfxr 41616 etransclem17 42413 etransclem46 42442 etransclem47 42443 2zrngagrp 44142 digval 44586 |
Copyright terms: Public domain | W3C validator |