Theorem negex 11391

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  0cc0 11038   − cmin 11377  -cneg 11378

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 2708  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 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-v 3431  df-dif 3892  df-un 3894  df-ss 3906  df-nul 4274  df-sn 4568  df-pr 4570  df-uni 4851  df-iota 6454  df-fv 6506  df-ov 7370  df-neg 11380

This theorem is referenced by:  negiso  12136  infrenegsup  12139  xnegex  13160  ceilval  13797  monoord2  13995  m1expcl2  14047  sgnval  15050  infcvgaux1i  15822  infcvgaux2i  15823  cnmsgnsubg  21557  evth2  24927  ivth2  25422  mbfinf  25632  mbfi1flimlem  25689  i1fibl  25775  ditgex  25819  dvrec  25922  dvmptsub  25934  dvexp3  25945  rolle  25957  dvlipcn  25961  dvivth  25977  lhop2  25982  dvfsumge  25989  ftc2  26011  plyremlem  26270  advlogexp  26619  logtayl  26624  logccv  26627  dvatan  26899  amgmlem  26953  emcllem7  26965  basellem9  27052  addsqnreup  27406  axlowdimlem7  29017  axlowdimlem8  29018  axlowdimlem9  29019  axlowdimlem13  29023  sgncl  32904  sgnsval  33222  sgnsf  33223  xrge0iifcv  34078  xrge0iifiso  34079  xrge0iifhom  34081  dvtan  37991  ftc1anclem5  38018  ftc1anclem6  38019  ftc2nc  38023  areacirclem1  38029  readvrec  42794  monotoddzzfi  43370  monotoddzz  43371  oddcomabszz  43372  rngunsnply  43597  infnsuprnmpt  45679  liminfltlem  46232  dvcosax  46354  itgsin0pilem1  46378  fourierdlem41  46576  fourierdlem48  46582  fourierdlem102  46636  fourierdlem114  46648  fourierswlem  46658  hoicvr  46976  hoicvrrex  46984  smfliminflem  47258  zlmodzxzldeplem3  48978  amgmwlem  50277