Theorem negex 11379

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 11368	. 2 ⊢ -𝐴 = (0 − 𝐴)
2	1	ovexi 7387	1 ⊢ -𝐴 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438  0cc0 11028   − cmin 11365  -cneg 11366

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5248

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-sn 4580  df-pr 4582  df-uni 4862  df-iota 6442  df-fv 6494  df-ov 7356  df-neg 11368

This theorem is referenced by:  negiso  12123  infrenegsup  12126  xnegex  13128  ceilval  13760  monoord2  13958  m1expcl2  14010  sgnval  15013  infcvgaux1i  15782  infcvgaux2i  15783  cnmsgnsubg  21502  evth2  24875  ivth2  25372  mbfinf  25582  mbfi1flimlem  25639  i1fibl  25725  ditgex  25769  dvrec  25875  dvmptsub  25887  dvexp3  25898  rolle  25910  dvlipcn  25915  dvivth  25931  lhop2  25936  dvfsumge  25944  ftc2  25967  plyremlem  26228  advlogexp  26580  logtayl  26585  logccv  26588  dvatan  26861  amgmlem  26916  emcllem7  26928  basellem9  27015  addsqnreup  27370  axlowdimlem7  28911  axlowdimlem8  28912  axlowdimlem9  28913  axlowdimlem13  28917  sgncl  32789  sgnsval  33116  sgnsf  33117  xrge0iifcv  33900  xrge0iifiso  33901  xrge0iifhom  33903  dvtan  37649  ftc1anclem5  37676  ftc1anclem6  37677  ftc2nc  37681  areacirclem1  37687  readvrec  42335  monotoddzzfi  42915  monotoddzz  42916  oddcomabszz  42917  rngunsnply  43142  infnsuprnmpt  45228  liminfltlem  45786  dvcosax  45908  itgsin0pilem1  45932  fourierdlem41  46130  fourierdlem48  46136  fourierdlem102  46190  fourierdlem114  46202  fourierswlem  46212  hoicvr  46530  hoicvrrex  46538  smfliminflem  46812  zlmodzxzldeplem3  48488  amgmwlem  49788