Theorem negex 10927

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

Syntax hints:   ∈ wcel 2111  Vcvv 3409  0cc0 10580   − cmin 10913  -cneg 10914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-nul 5179

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-ral 3075  df-rex 3076  df-v 3411  df-sbc 3699  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-sn 4526  df-pr 4528  df-uni 4802  df-iota 6298  df-fv 6347  df-ov 7158  df-neg 10916

This theorem is referenced by:  negiso  11662  infrenegsup  11665  xnegex  12647  ceilval  13262  monoord2  13456  m1expcl2  13506  sgnval  14500  infcvgaux1i  15265  infcvgaux2i  15266  cnmsgnsubg  20347  evth2  23666  ivth2  24160  mbfinf  24370  mbfi1flimlem  24427  i1fibl  24512  ditgex  24556  dvrec  24659  dvmptsub  24671  dvexp3  24682  rolle  24694  dvlipcn  24698  dvivth  24714  lhop2  24719  dvfsumge  24726  ftc2  24748  plyremlem  25004  advlogexp  25350  logtayl  25355  logccv  25358  dvatan  25625  amgmlem  25679  emcllem7  25691  basellem9  25778  addsqnreup  26131  axlowdimlem7  26846  axlowdimlem8  26847  axlowdimlem9  26848  axlowdimlem13  26852  sgnsval  30958  sgnsf  30959  xrge0iifcv  31409  xrge0iifiso  31410  xrge0iifhom  31412  sgncl  32028  dvtan  35413  ftc1anclem5  35440  ftc1anclem6  35441  ftc2nc  35445  areacirclem1  35451  monotoddzzfi  40284  monotoddzz  40285  oddcomabszz  40286  rngunsnply  40518  infnsuprnmpt  42284  liminfltlem  42840  dvcosax  42962  itgsin0pilem1  42986  fourierdlem41  43184  fourierdlem48  43190  fourierdlem102  43244  fourierdlem114  43256  fourierswlem  43266  hoicvr  43581  hoicvrrex  43589  smfliminflem  43855  zlmodzxzldeplem3  45304  amgmwlem  45794