![]() |
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 6930 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 10609 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 10609 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2839 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 (class class class)co 6922 0cc0 10272 − cmin 10606 -cneg 10607 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-rex 3096 df-rab 3099 df-v 3400 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-iota 6099 df-fv 6143 df-ov 6925 df-neg 10609 |
This theorem is referenced by: negeqi 10615 negeqd 10616 neg11 10674 renegcl 10686 negn0 10804 negf1o 10805 negfi 11325 fiminre 11326 infm3lem 11335 infm3 11336 riotaneg 11356 negiso 11357 infrenegsup 11360 elz 11730 elz2 11745 znegcl 11764 zindd 11830 zriotaneg 11843 ublbneg 12080 eqreznegel 12081 supminf 12082 zsupss 12084 qnegcl 12113 xnegeq 12350 ceilval 12958 expneg 13186 m1expcl2 13200 sqeqor 13297 sqrmo 14399 dvdsnegb 15406 lcmneg 15722 pcexp 15968 pcneg 15982 mulgneg2 17960 negfcncf 23130 xrhmeo 23153 evth2 23167 volsup2 23809 mbfi1fseqlem2 23920 mbfi1fseq 23925 lhop2 24215 lognegb 24773 lgsdir2lem4 25505 rpvmasum2 25653 ex-ceil 27880 hgt749d 31329 itgaddnclem2 34094 ftc1anclem5 34114 areacirc 34130 renegclALT 35117 rexzrexnn0 38328 dvdsrabdioph 38334 monotoddzzfi 38466 monotoddzz 38467 oddcomabszz 38468 infnsuprnmpt 40376 supminfrnmpt 40578 supminfxr 40599 etransclem17 41395 etransclem46 41424 etransclem47 41425 2zrngagrp 42958 digval 43407 |
Copyright terms: Public domain | W3C validator |