MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  negex Structured version   Unicode version

Theorem negex 9608
Description: A negative is a set. (Contributed by NM, 4-Apr-2005.)
Assertion
Ref Expression
negex  |-  -u A  e.  _V

Proof of Theorem negex
StepHypRef Expression
1 df-neg 9598 . 2  |-  -u A  =  ( 0  -  A )
2 ovex 6116 . 2  |-  ( 0  -  A )  e. 
_V
31, 2eqeltri 2513 1  |-  -u A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2972  (class class class)co 6091   0cc0 9282    - cmin 9595   -ucneg 9596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-nul 4421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-sn 3878  df-pr 3880  df-uni 4092  df-iota 5381  df-fv 5426  df-ov 6094  df-neg 9598
This theorem is referenced by:  negiso  10306  infmsup  10308  xnegex  11178  ceilval  11679  monoord2  11837  m1expcl2  11887  sgnval  12577  infcvgaux1i  13319  infcvgaux2i  13320  cnmsgnsubg  18007  evth2  20532  ivth2  20939  mbfinf  21143  mbfi1flimlem  21200  i1fibl  21285  ditgex  21327  dvrec  21429  dvmptsub  21441  dvexp3  21450  rolle  21462  dvlipcn  21466  dvivth  21482  lhop2  21487  dvfsumge  21494  ftc2  21516  plyremlem  21770  advlogexp  22100  logtayl  22105  logccv  22108  dvatan  22330  amgmlem  22383  emcllem7  22395  axlowdimlem7  23194  axlowdimlem8  23195  axlowdimlem9  23196  axlowdimlem13  23200  sgnsval  26191  sgnsf  26192  xrge0iifcv  26364  xrge0iifiso  26365  xrge0iifhom  26367  sgncl  26921  dvtan  28442  ftc1anclem5  28471  ftc1anclem6  28472  ftc2nc  28476  areacirclem1  28484  monotoddzzfi  29283  monotoddzz  29284  oddcomabszz  29285  rngunsnply  29530  itgsin0pilem1  29790  zlmodzxzldeplem3  31044
  Copyright terms: Public domain W3C validator