Theorem negex 11443

Description: A negative is a set. (Contributed by NM, 4-Apr-2005.)

Assertion

Ref	Expression
negex	⊢ -𝐴 ∈ V

Proof of Theorem negex

Step	Hyp	Ref	Expression
1		df-neg 11432	. 2 ⊢ -𝐴 = (0 − 𝐴)
2	1	ovexi 7434	1 ⊢ -𝐴 ∈ V

Syntax hints:   ∈ wcel 2145  Vcvv 3457  0cc0 11088   − cmin 11429  -cneg 11430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-nul 5261

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-sn 4586  df-pr 4588  df-uni 4869  df-iota 6481  df-fv 6533  df-ov 7403  df-neg 11432

This theorem is referenced by:  negiso  12186  infrenegsup  12189  xnegex  13225  ceilval  13862  monoord2  14060  m1expcl2  14112  sgnval  15115  sgndm  15123  sgncl  15124  infcvgaux1i  15901  infcvgaux2i  15902  cnmsgnsubg  21687  evth2  25080  ivth2  25575  mbfinf  25785  mbfi1flimlem  25842  i1fibl  25928  ditgex  25972  dvrec  26075  dvmptsub  26087  dvexp3  26098  rolle  26110  dvlipcn  26114  dvivth  26130  lhop2  26135  dvfsumge  26142  ftc2  26164  plyremlem  26426  advlogexp  26778  logtayl  26783  logccv  26786  dvatan  27058  amgmlem  27112  emcllem7  27124  basellem9  27211  addsqnreup  27565  axlowdimlem7  29207  axlowdimlem8  29208  axlowdimlem9  29209  axlowdimlem13  29213  sgnsval  33394  sgnsf  33395  xrge0iifcv  34241  xrge0iifiso  34242  xrge0iifhom  34244  dvtan  38181  ftc1anclem5  38208  ftc1anclem6  38209  ftc2nc  38213  areacirclem1  38219  readvrec  42983  monotoddzzfi  43531  monotoddzz  43532  oddcomabszz  43533  rngunsnply  43758  infnsuprnmpt  45823  liminfltlem  46376  dvcosax  46498  itgsin0pilem1  46522  fourierdlem41  46720  fourierdlem48  46726  fourierdlem102  46780  fourierdlem114  46792  fourierswlem  46802  hoicvr  47120  hoicvrrex  47128  smfliminflem  47402  zlmodzxzldeplem3  49133  amgmwlem  50431