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

Theorem negex 9809
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 9799 . 2  |-  -u A  =  ( 0  -  A )
2 ovex 6298 . 2  |-  ( 0  -  A )  e. 
_V
31, 2eqeltri 2538 1  |-  -u A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   _Vcvv 3106  (class class class)co 6270   0cc0 9481    - cmin 9796   -ucneg 9797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-nul 4568
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-ral 2809  df-rex 2810  df-v 3108  df-sbc 3325  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-sn 4017  df-pr 4019  df-uni 4236  df-iota 5534  df-fv 5578  df-ov 6273  df-neg 9799
This theorem is referenced by:  negiso  10514  infmsup  10516  xnegex  11410  ceilval  11949  monoord2  12120  m1expcl2  12170  sgnval  13003  infcvgaux1i  13750  infcvgaux2i  13751  cnmsgnsubg  18786  evth2  21626  ivth2  22033  mbfinf  22238  mbfi1flimlem  22295  i1fibl  22380  ditgex  22422  dvrec  22524  dvmptsub  22536  dvexp3  22545  rolle  22557  dvlipcn  22561  dvivth  22577  lhop2  22582  dvfsumge  22589  ftc2  22611  plyremlem  22866  advlogexp  23204  logtayl  23209  logccv  23212  dvatan  23463  amgmlem  23517  emcllem7  23529  basellem9  23560  axlowdimlem7  24453  axlowdimlem8  24454  axlowdimlem9  24455  axlowdimlem13  24459  sgnsval  27952  sgnsf  27953  xrge0iifcv  28151  xrge0iifiso  28152  xrge0iifhom  28154  sgncl  28741  dvtan  30305  ftc1anclem5  30334  ftc1anclem6  30335  ftc2nc  30339  areacirclem1  30347  monotoddzzfi  31117  monotoddzz  31118  oddcomabszz  31119  rngunsnply  31363  dvcosax  31962  itgsin0pilem1  31987  fourierdlem41  32169  fourierdlem48  32176  fourierdlem102  32230  fourierdlem114  32242  fourierswlem  32252  zlmodzxzldeplem3  33357
  Copyright terms: Public domain W3C validator