Theorem negex 11202

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

Syntax hints:   ∈ wcel 2109  Vcvv 3430  0cc0 10855   − cmin 11188  -cneg 11189

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-nul 5233

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-sn 4567  df-pr 4569  df-uni 4845  df-iota 6388  df-fv 6438  df-ov 7271  df-neg 11191

This theorem is referenced by:  negiso  11938  infrenegsup  11941  xnegex  12924  ceilval  13539  monoord2  13735  m1expcl2  13785  sgnval  14780  infcvgaux1i  15550  infcvgaux2i  15551  cnmsgnsubg  20763  evth2  24104  ivth2  24600  mbfinf  24810  mbfi1flimlem  24868  i1fibl  24953  ditgex  24997  dvrec  25100  dvmptsub  25112  dvexp3  25123  rolle  25135  dvlipcn  25139  dvivth  25155  lhop2  25160  dvfsumge  25167  ftc2  25189  plyremlem  25445  advlogexp  25791  logtayl  25796  logccv  25799  dvatan  26066  amgmlem  26120  emcllem7  26132  basellem9  26219  addsqnreup  26572  axlowdimlem7  27297  axlowdimlem8  27298  axlowdimlem9  27299  axlowdimlem13  27303  sgnsval  31407  sgnsf  31408  xrge0iifcv  31863  xrge0iifiso  31864  xrge0iifhom  31866  sgncl  32484  dvtan  35806  ftc1anclem5  35833  ftc1anclem6  35834  ftc2nc  35838  areacirclem1  35844  monotoddzzfi  40744  monotoddzz  40745  oddcomabszz  40746  rngunsnply  40978  infnsuprnmpt  42749  liminfltlem  43299  dvcosax  43421  itgsin0pilem1  43445  fourierdlem41  43643  fourierdlem48  43649  fourierdlem102  43703  fourierdlem114  43715  fourierswlem  43725  hoicvr  44040  hoicvrrex  44048  smfliminflem  44314  zlmodzxzldeplem3  45795  amgmwlem  46458