![]() |
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 6698 | . 2 ⊢ (𝐴 = 𝐵 → (0 − 𝐴) = (0 − 𝐵)) | |
2 | df-neg 10307 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
3 | df-neg 10307 | . 2 ⊢ -𝐵 = (0 − 𝐵) | |
4 | 1, 2, 3 | 3eqtr4g 2710 | 1 ⊢ (𝐴 = 𝐵 → -𝐴 = -𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 (class class class)co 6690 0cc0 9974 − cmin 10304 -cneg 10305 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-rex 2947 df-rab 2950 df-v 3233 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-iota 5889 df-fv 5934 df-ov 6693 df-neg 10307 |
This theorem is referenced by: negeqi 10312 negeqd 10313 neg11 10370 renegcl 10382 negn0 10497 negf1o 10498 negfi 11009 fiminre 11010 infm3lem 11019 infm3 11020 riotaneg 11040 negiso 11041 infrenegsup 11044 elz 11417 elz2 11432 znegcl 11450 zindd 11516 zriotaneg 11529 ublbneg 11811 eqreznegel 11812 supminf 11813 zsupss 11815 qnegcl 11843 xnegeq 12076 ceilval 12679 expneg 12908 m1expcl2 12922 sqeqor 13018 sqrmo 14036 dvdsnegb 15046 lcmneg 15363 pcexp 15611 pcneg 15625 mulgneg2 17622 negfcncf 22769 xrhmeo 22792 evth2 22806 volsup2 23419 mbfi1fseqlem2 23528 mbfi1fseq 23533 lhop2 23823 lognegb 24381 lgsdir2lem4 25098 rpvmasum2 25246 ex-ceil 27435 hgt749d 30855 itgaddnclem2 33599 ftc1anclem5 33619 areacirc 33635 renegclALT 34567 rexzrexnn0 37685 dvdsrabdioph 37691 monotoddzzfi 37824 monotoddzz 37825 oddcomabszz 37826 infnsuprnmpt 39779 supminfrnmpt 39985 supminfxr 40007 etransclem17 40786 etransclem46 40815 etransclem47 40816 2zrngagrp 42268 digval 42717 |
Copyright terms: Public domain | W3C validator |