Theorem negex 11458

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  0cc0 11110   − cmin 11444  -cneg 11445

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-sn 4630  df-pr 4632  df-uni 4910  df-iota 6496  df-fv 6552  df-ov 7412  df-neg 11447

This theorem is referenced by:  negiso  12194  infrenegsup  12197  xnegex  13187  ceilval  13803  monoord2  13999  m1expcl2  14051  sgnval  15035  infcvgaux1i  15803  infcvgaux2i  15804  cnmsgnsubg  21130  evth2  24476  ivth2  24972  mbfinf  25182  mbfi1flimlem  25240  i1fibl  25325  ditgex  25369  dvrec  25472  dvmptsub  25484  dvexp3  25495  rolle  25507  dvlipcn  25511  dvivth  25527  lhop2  25532  dvfsumge  25539  ftc2  25561  plyremlem  25817  advlogexp  26163  logtayl  26168  logccv  26171  dvatan  26440  amgmlem  26494  emcllem7  26506  basellem9  26593  addsqnreup  26946  axlowdimlem7  28206  axlowdimlem8  28207  axlowdimlem9  28208  axlowdimlem13  28212  sgnsval  32320  sgnsf  32321  xrge0iifcv  32914  xrge0iifiso  32915  xrge0iifhom  32917  sgncl  33537  dvtan  36538  ftc1anclem5  36565  ftc1anclem6  36566  ftc2nc  36570  areacirclem1  36576  monotoddzzfi  41681  monotoddzz  41682  oddcomabszz  41683  rngunsnply  41915  infnsuprnmpt  43954  liminfltlem  44520  dvcosax  44642  itgsin0pilem1  44666  fourierdlem41  44864  fourierdlem48  44870  fourierdlem102  44924  fourierdlem114  44936  fourierswlem  44946  hoicvr  45264  hoicvrrex  45272  smfliminflem  45546  zlmodzxzldeplem3  47183  amgmwlem  47849