Theorem negex 11585

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  0cc0 11230   − cmin 11571   -cneg 11572

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-nul 5264

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591  df-uni 4871  df-iota 6515  df-fv 6569  df-ov 7449  df-neg 11574

This theorem is used by:  negiso  12327  infrenegsup  12330  xnegex  13368  ceilval  14008  monoord2  14206  m1expcl2  14258  sgnval  15273  sgndm  15281  sgncl  15282  infcvgaux1i  16058  infcvgaux2i  16059  cnmsgnsubg  21916  evth2  25314  ivth2  25809  mbfinf  26019  mbfi1flimlem  26076  i1fibl  26161  ditgex  26205  dvrec  26308  dvmptsub  26320  dvexp3  26331  rolle  26343  dvlipcn  26347  dvivth  26363  lhop2  26368  dvfsumge  26375  ftc2  26397  plyremlem  26658  advlogexp  27016  logtayl  27021  logccv  27024  dvatan  27296  amgmlem  27350  emcllem7  27362  basellem9  27449  addsqnreup  27803  axlowdimlem7  29559  axlowdimlem8  29560  axlowdimlem9  29561  axlowdimlem13  29565  sgnsval  33798  sgnsf  33799  xrge0iifcv  34649  xrge0iifiso  34650  xrge0iifhom  34652  dvtan  38793  ftc1anclem5  38820  ftc1anclem6  38821  ftc2nc  38825  areacirclem1  38831  readvrec  43617  monotoddzzfi  44153  monotoddzz  44154  oddcomabszz  44155  rngunsnply  44374  infnsuprnmpt  46477  liminfltlem  47029  dvcosax  47151  itgsin0pilem1  47175  fourierdlem41  47373  fourierdlem48  47379  fourierdlem102  47433  fourierdlem114  47445  fourierswlem  47455  hoicvr  47773  hoicvrrex  47781  smfliminflem  48055  zlmodzxzldeplem3  49829  crosspaltd  51278  amgmwlem  51299