Theorem negex 10878

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

Syntax hints:   ∈ wcel 2110  Vcvv 3494  0cc0 10531   − cmin 10864  -cneg 10865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-nul 5202

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-sn 4561  df-pr 4563  df-uni 4832  df-iota 6308  df-fv 6357  df-ov 7153  df-neg 10867

This theorem is referenced by:  negiso  11615  infrenegsup  11618  xnegex  12595  ceilval  13202  monoord2  13395  m1expcl2  13445  sgnval  14441  infcvgaux1i  15206  infcvgaux2i  15207  cnmsgnsubg  20715  evth2  23558  ivth2  24050  mbfinf  24260  mbfi1flimlem  24317  i1fibl  24402  ditgex  24444  dvrec  24546  dvmptsub  24558  dvexp3  24569  rolle  24581  dvlipcn  24585  dvivth  24601  lhop2  24606  dvfsumge  24613  ftc2  24635  plyremlem  24887  advlogexp  25232  logtayl  25237  logccv  25240  dvatan  25507  amgmlem  25561  emcllem7  25573  basellem9  25660  addsqnreup  26013  axlowdimlem7  26728  axlowdimlem8  26729  axlowdimlem9  26730  axlowdimlem13  26734  sgnsval  30798  sgnsf  30799  xrge0iifcv  31172  xrge0iifiso  31173  xrge0iifhom  31175  sgncl  31791  dvtan  34936  ftc1anclem5  34965  ftc1anclem6  34966  ftc2nc  34970  areacirclem1  34976  monotoddzzfi  39532  monotoddzz  39533  oddcomabszz  39534  rngunsnply  39766  infnsuprnmpt  41515  liminfltlem  42078  dvcosax  42204  itgsin0pilem1  42228  fourierdlem41  42427  fourierdlem48  42433  fourierdlem102  42487  fourierdlem114  42499  fourierswlem  42509  hoicvr  42824  hoicvrrex  42832  smfliminflem  43098  zlmodzxzldeplem3  44551  amgmwlem  44897