Theorem negex 11382

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  0cc0 11029   − cmin 11368  -cneg 11369

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-sn 4569  df-pr 4571  df-uni 4852  df-iota 6448  df-fv 6500  df-ov 7363  df-neg 11371

This theorem is referenced by:  negiso  12127  infrenegsup  12130  xnegex  13151  ceilval  13788  monoord2  13986  m1expcl2  14038  sgnval  15041  infcvgaux1i  15813  infcvgaux2i  15814  cnmsgnsubg  21567  evth2  24937  ivth2  25432  mbfinf  25642  mbfi1flimlem  25699  i1fibl  25785  ditgex  25829  dvrec  25932  dvmptsub  25944  dvexp3  25955  rolle  25967  dvlipcn  25971  dvivth  25987  lhop2  25992  dvfsumge  25999  ftc2  26021  plyremlem  26281  advlogexp  26632  logtayl  26637  logccv  26640  dvatan  26912  amgmlem  26967  emcllem7  26979  basellem9  27066  addsqnreup  27420  axlowdimlem7  29031  axlowdimlem8  29032  axlowdimlem9  29033  axlowdimlem13  29037  sgncl  32919  sgnsval  33237  sgnsf  33238  xrge0iifcv  34094  xrge0iifiso  34095  xrge0iifhom  34097  dvtan  38005  ftc1anclem5  38032  ftc1anclem6  38033  ftc2nc  38037  areacirclem1  38043  readvrec  42808  monotoddzzfi  43388  monotoddzz  43389  oddcomabszz  43390  rngunsnply  43615  infnsuprnmpt  45697  liminfltlem  46250  dvcosax  46372  itgsin0pilem1  46396  fourierdlem41  46594  fourierdlem48  46600  fourierdlem102  46654  fourierdlem114  46666  fourierswlem  46676  hoicvr  46994  hoicvrrex  47002  smfliminflem  47276  zlmodzxzldeplem3  48990  amgmwlem  50289