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

Theorem negex 9818
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 9808 . 2  |-  -u A  =  ( 0  -  A )
2 ovex 6305 . 2  |-  ( 0  -  A )  e. 
_V
31, 2eqeltri 2525 1  |-  -u A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1802   _Vcvv 3093  (class class class)co 6277   0cc0 9490    - cmin 9805   -ucneg 9806
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-nul 4562
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-ral 2796  df-rex 2797  df-v 3095  df-sbc 3312  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-sn 4011  df-pr 4013  df-uni 4231  df-iota 5537  df-fv 5582  df-ov 6280  df-neg 9808
This theorem is referenced by:  negiso  10520  infmsup  10522  xnegex  11411  ceilval  11941  monoord2  12112  m1expcl2  12162  sgnval  12895  infcvgaux1i  13642  infcvgaux2i  13643  cnmsgnsubg  18480  evth2  21326  ivth2  21733  mbfinf  21938  mbfi1flimlem  21995  i1fibl  22080  ditgex  22122  dvrec  22224  dvmptsub  22236  dvexp3  22245  rolle  22257  dvlipcn  22261  dvivth  22277  lhop2  22282  dvfsumge  22289  ftc2  22311  plyremlem  22565  advlogexp  22901  logtayl  22906  logccv  22909  dvatan  23131  amgmlem  23184  emcllem7  23196  basellem9  23227  axlowdimlem7  24116  axlowdimlem8  24117  axlowdimlem9  24118  axlowdimlem13  24122  sgnsval  27584  sgnsf  27585  xrge0iifcv  27782  xrge0iifiso  27783  xrge0iifhom  27785  sgncl  28343  dvtan  30033  ftc1anclem5  30062  ftc1anclem6  30063  ftc2nc  30067  areacirclem1  30075  monotoddzzfi  30846  monotoddzz  30847  oddcomabszz  30848  rngunsnply  31091  dvcosax  31623  itgsin0pilem1  31634  fourierdlem41  31815  fourierdlem48  31822  fourierdlem102  31876  fourierdlem114  31888  fourierswlem  31898  zlmodzxzldeplem3  32813
  Copyright terms: Public domain W3C validator