![]() |
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 11434 | . 2 ⊢ -𝐴 = (0 − 𝐴) | |
2 | 1 | ovexi 7430 | 1 ⊢ -𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2107 Vcvv 3475 0cc0 11097 − cmin 11431 -cneg 11432 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 ax-nul 5302 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2942 df-v 3477 df-dif 3949 df-un 3951 df-in 3953 df-ss 3963 df-nul 4321 df-sn 4625 df-pr 4627 df-uni 4905 df-iota 6487 df-fv 6543 df-ov 7399 df-neg 11434 |
This theorem is referenced by: negiso 12181 infrenegsup 12184 xnegex 13174 ceilval 13790 monoord2 13986 m1expcl2 14038 sgnval 15022 infcvgaux1i 15790 infcvgaux2i 15791 cnmsgnsubg 21103 evth2 24445 ivth2 24941 mbfinf 25151 mbfi1flimlem 25209 i1fibl 25294 ditgex 25338 dvrec 25441 dvmptsub 25453 dvexp3 25464 rolle 25476 dvlipcn 25480 dvivth 25496 lhop2 25501 dvfsumge 25508 ftc2 25530 plyremlem 25786 advlogexp 26132 logtayl 26137 logccv 26140 dvatan 26407 amgmlem 26461 emcllem7 26473 basellem9 26560 addsqnreup 26913 axlowdimlem7 28173 axlowdimlem8 28174 axlowdimlem9 28175 axlowdimlem13 28179 sgnsval 32291 sgnsf 32292 xrge0iifcv 32845 xrge0iifiso 32846 xrge0iifhom 32848 sgncl 33468 dvtan 36443 ftc1anclem5 36470 ftc1anclem6 36471 ftc2nc 36475 areacirclem1 36481 monotoddzzfi 41552 monotoddzz 41553 oddcomabszz 41554 rngunsnply 41786 infnsuprnmpt 43827 liminfltlem 44393 dvcosax 44515 itgsin0pilem1 44539 fourierdlem41 44737 fourierdlem48 44743 fourierdlem102 44797 fourierdlem114 44809 fourierswlem 44819 hoicvr 45137 hoicvrrex 45145 smfliminflem 45419 zlmodzxzldeplem3 47023 amgmwlem 47689 |
Copyright terms: Public domain | W3C validator |