Theorem negex 11378

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  0cc0 11026   − cmin 11364  -cneg 11365

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-nul 5251

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-sn 4581  df-pr 4583  df-uni 4864  df-iota 6448  df-fv 6500  df-ov 7361  df-neg 11367

This theorem is referenced by:  negiso  12122  infrenegsup  12125  xnegex  13123  ceilval  13758  monoord2  13956  m1expcl2  14008  sgnval  15011  infcvgaux1i  15780  infcvgaux2i  15781  cnmsgnsubg  21532  evth2  24915  ivth2  25412  mbfinf  25622  mbfi1flimlem  25679  i1fibl  25765  ditgex  25809  dvrec  25915  dvmptsub  25927  dvexp3  25938  rolle  25950  dvlipcn  25955  dvivth  25971  lhop2  25976  dvfsumge  25984  ftc2  26007  plyremlem  26268  advlogexp  26620  logtayl  26625  logccv  26628  dvatan  26901  amgmlem  26956  emcllem7  26968  basellem9  27055  addsqnreup  27410  axlowdimlem7  29021  axlowdimlem8  29022  axlowdimlem9  29023  axlowdimlem13  29027  sgncl  32912  sgnsval  33243  sgnsf  33244  xrge0iifcv  34091  xrge0iifiso  34092  xrge0iifhom  34094  dvtan  37867  ftc1anclem5  37894  ftc1anclem6  37895  ftc2nc  37899  areacirclem1  37905  readvrec  42613  monotoddzzfi  43180  monotoddzz  43181  oddcomabszz  43182  rngunsnply  43407  infnsuprnmpt  45490  liminfltlem  46044  dvcosax  46166  itgsin0pilem1  46190  fourierdlem41  46388  fourierdlem48  46394  fourierdlem102  46448  fourierdlem114  46460  fourierswlem  46470  hoicvr  46788  hoicvrrex  46796  smfliminflem  47070  zlmodzxzldeplem3  48744  amgmwlem  50043