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

Theorem negex 9304
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 9294 . 2  |-  -u A  =  ( 0  -  A )
2 ovex 6106 . 2  |-  ( 0  -  A )  e. 
_V
31, 2eqeltri 2506 1  |-  -u A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1725   _Vcvv 2956  (class class class)co 6081   0cc0 8990    - cmin 9291   -ucneg 9292
This theorem is referenced by:  negiso  9984  infmsup  9986  xnegex  10794  monoord2  11354  m1expcl2  11403  infcvgaux1i  12636  infcvgaux2i  12637  evth2  18985  ivth2  19352  mbfinf  19557  mbfi1flimlem  19614  i1fibl  19699  ditgex  19739  dvrec  19841  dvmptsub  19853  dvexp3  19862  rolle  19874  dvlipcn  19878  dvivth  19894  lhop2  19899  dvfsumge  19906  ftc2  19928  plyremlem  20221  advlogexp  20546  logtayl  20551  logccv  20554  dvatan  20775  amgmlem  20828  emcllem7  20840  xrge0iifcv  24320  xrge0iifiso  24321  xrge0iifhom  24323  axlowdimlem7  25887  axlowdimlem8  25888  axlowdimlem9  25889  axlowdimlem13  25893  ftc1anclem5  26284  ftc1anclem6  26285  ftc2nc  26289  dvreasin  26290  areacirclem1  26292  monotoddzzfi  27005  monotoddzz  27006  oddcomabszz  27007  rngunsnply  27355  cnmsgnsubg  27411  itgsin0pilem1  27720  sgnval  28518  ceilingval  28528
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-nul 4338
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-ral 2710  df-rex 2711  df-v 2958  df-sbc 3162  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-sn 3820  df-pr 3821  df-uni 4016  df-iota 5418  df-fv 5462  df-ov 6084  df-neg 9294
  Copyright terms: Public domain W3C validator