Theorem negex 11480

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  0cc0 11129   − cmin 11466  -cneg 11467

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-nul 5276

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884  df-iota 6484  df-fv 6539  df-ov 7408  df-neg 11469

This theorem is referenced by:  negiso  12222  infrenegsup  12225  xnegex  13224  ceilval  13855  monoord2  14051  m1expcl2  14103  sgnval  15107  infcvgaux1i  15873  infcvgaux2i  15874  cnmsgnsubg  21537  evth2  24910  ivth2  25408  mbfinf  25618  mbfi1flimlem  25675  i1fibl  25761  ditgex  25805  dvrec  25911  dvmptsub  25923  dvexp3  25934  rolle  25946  dvlipcn  25951  dvivth  25967  lhop2  25972  dvfsumge  25980  ftc2  26003  plyremlem  26264  advlogexp  26616  logtayl  26621  logccv  26624  dvatan  26897  amgmlem  26952  emcllem7  26964  basellem9  27051  addsqnreup  27406  axlowdimlem7  28927  axlowdimlem8  28928  axlowdimlem9  28929  axlowdimlem13  28933  sgncl  32810  sgnsval  33172  sgnsf  33173  xrge0iifcv  33965  xrge0iifiso  33966  xrge0iifhom  33968  dvtan  37694  ftc1anclem5  37721  ftc1anclem6  37722  ftc2nc  37726  areacirclem1  37732  readvrec  42405  monotoddzzfi  42966  monotoddzz  42967  oddcomabszz  42968  rngunsnply  43193  infnsuprnmpt  45274  liminfltlem  45833  dvcosax  45955  itgsin0pilem1  45979  fourierdlem41  46177  fourierdlem48  46183  fourierdlem102  46237  fourierdlem114  46249  fourierswlem  46259  hoicvr  46577  hoicvrrex  46585  smfliminflem  46859  zlmodzxzldeplem3  48478  amgmwlem  49666