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

Theorem negex 9819
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 9809 . 2  |-  -u A  =  ( 0  -  A )
2 ovex 6272 . 2  |-  ( 0  -  A )  e. 
_V
31, 2eqeltri 2497 1  |-  -u A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   _Vcvv 3017  (class class class)co 6244   0cc0 9485    - cmin 9806   -ucneg 9807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403  ax-nul 4493
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2275  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-ne 2596  df-ral 2714  df-rex 2715  df-v 3019  df-sbc 3238  df-dif 3377  df-un 3379  df-in 3381  df-ss 3388  df-nul 3700  df-sn 3937  df-pr 3939  df-uni 4158  df-iota 5503  df-fv 5547  df-ov 6247  df-neg 9809
This theorem is referenced by:  negiso  10533  infrenegsup  10537  infmsupOLD  10538  xnegex  11447  ceilval  12012  monoord2  12189  m1expcl2  12239  sgnval  13090  infcvgaux1i  13853  infcvgaux2i  13854  cnmsgnsubg  19082  evth2  21925  ivth2  22343  mbfinf  22558  mbfinfOLD  22559  mbfi1flimlem  22617  i1fibl  22702  ditgex  22744  dvrec  22846  dvmptsub  22858  dvexp3  22867  rolle  22879  dvlipcn  22883  dvivth  22899  lhop2  22904  dvfsumge  22911  ftc2  22933  plyremlem  23194  advlogexp  23537  logtayl  23542  logccv  23545  dvatan  23798  amgmlem  23852  emcllem7  23864  basellem9  23952  axlowdimlem7  24915  axlowdimlem8  24916  axlowdimlem9  24917  axlowdimlem13  24921  sgnsval  28437  sgnsf  28438  xrge0iifcv  28687  xrge0iifiso  28688  xrge0iifhom  28690  sgncl  29356  dvtan  31899  ftc1anclem5  31928  ftc1anclem6  31929  ftc2nc  31933  areacirclem1  31939  monotoddzzfi  35703  monotoddzz  35704  oddcomabszz  35705  rngunsnply  35952  dvcosax  37681  itgsin0pilem1  37709  fourierdlem41  37894  fourierdlem48  37901  fourierdlem102  37955  fourierdlem114  37967  fourierswlem  37977  hoicvr  38217  hoicvrrex  38225  zlmodzxzldeplem3  39888
  Copyright terms: Public domain W3C validator