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 7158 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 10867 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 10867 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2881 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 (class class class)co 7150 0cc0 10531 − cmin 10864 -cneg 10865 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1907 ax-6 1966 ax-7 2011 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2157 ax-12 2173 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1536 df-ex 1777 df-nf 1781 df-sb 2066 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rex 3144 df-rab 3147 df-v 3496 df-dif 3938 df-un 3940 df-in 3942 df-ss 3951 df-nul 4291 df-if 4467 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5059 df-iota 6308 df-fv 6357 df-ov 7153 df-neg 10867 |
This theorem is referenced by: negeqi 10873 negeqd 10874 neg11 10931 renegcl 10943 negn0 11063 negf1o 11064 negfi 11583 fiminreOLD 11584 infm3lem 11593 infm3 11594 riotaneg 11614 negiso 11615 infrenegsup 11618 elz 11977 elz2 11993 znegcl 12011 zindd 12077 zriotaneg 12090 ublbneg 12327 eqreznegel 12328 supminf 12329 zsupss 12331 qnegcl 12359 xnegeq 12594 ceilval 13202 expneg 13431 m1expcl2 13445 sqeqor 13572 sqrmo 14605 dvdsnegb 15621 lcmneg 15941 pcexp 16190 pcneg 16204 mulgneg2 18255 negfcncf 23521 xrhmeo 23544 evth2 23558 volsup2 24200 mbfi1fseqlem2 24311 mbfi1fseq 24316 lhop2 24606 lognegb 25167 lgsdir2lem4 25898 rpvmasum2 26082 ex-ceil 28221 hgt749d 31915 itgaddnclem2 34945 ftc1anclem5 34965 areacirc 34981 renegclALT 36093 rexzrexnn0 39394 dvdsrabdioph 39400 monotoddzzfi 39532 monotoddzz 39533 oddcomabszz 39534 infnsuprnmpt 41515 supminfrnmpt 41712 supminfxr 41733 etransclem17 42530 etransclem46 42559 etransclem47 42560 2zrngagrp 44208 digval 44652 |
Copyright terms: Public domain | W3C validator |