![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > negex | Structured version Visualization version GIF version |
Description: A negative is a set. (Contributed by NM, 4-Apr-2005.) |
Ref | Expression |
---|---|
negex | ⊢ -𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-neg 11493 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
2 | 1 | ovexi 7465 | 1 ⊢ -𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3478 0cc0 11153 − cmin 11490 -cneg 11491 |
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 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 ax-nul 5312 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ne 2939 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-sn 4632 df-pr 4634 df-uni 4913 df-iota 6516 df-fv 6571 df-ov 7434 df-neg 11493 |
This theorem is referenced by: negiso 12246 infrenegsup 12249 xnegex 13247 ceilval 13875 monoord2 14071 m1expcl2 14123 sgnval 15124 infcvgaux1i 15890 infcvgaux2i 15891 cnmsgnsubg 21613 evth2 25006 ivth2 25504 mbfinf 25714 mbfi1flimlem 25772 i1fibl 25858 ditgex 25902 dvrec 26008 dvmptsub 26020 dvexp3 26031 rolle 26043 dvlipcn 26048 dvivth 26064 lhop2 26069 dvfsumge 26077 ftc2 26100 plyremlem 26361 advlogexp 26712 logtayl 26717 logccv 26720 dvatan 26993 amgmlem 27048 emcllem7 27060 basellem9 27147 addsqnreup 27502 axlowdimlem7 28978 axlowdimlem8 28979 axlowdimlem9 28980 axlowdimlem13 28984 sgnsval 33164 sgnsf 33165 xrge0iifcv 33895 xrge0iifiso 33896 xrge0iifhom 33898 sgncl 34520 dvtan 37657 ftc1anclem5 37684 ftc1anclem6 37685 ftc2nc 37689 areacirclem1 37695 readvrec 42371 monotoddzzfi 42931 monotoddzz 42932 oddcomabszz 42933 rngunsnply 43158 infnsuprnmpt 45195 liminfltlem 45760 dvcosax 45882 itgsin0pilem1 45906 fourierdlem41 46104 fourierdlem48 46110 fourierdlem102 46164 fourierdlem114 46176 fourierswlem 46186 hoicvr 46504 hoicvrrex 46512 smfliminflem 46786 zlmodzxzldeplem3 48348 amgmwlem 49033 |
Copyright terms: Public domain | W3C validator |