Theorem negex 11483

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  0cc0 11128   − cmin 11469  -cneg 11470

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

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 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-sn 4588  df-pr 4590  df-uni 4871  df-iota 6493  df-fv 6545  df-ov 7420  df-neg 11472

This theorem is used by:  negiso  12223  infrenegsup  12226  xnegex  13264  ceilval  13903  monoord2  14101  m1expcl2  14153  sgnval  15165  sgndm  15173  sgncl  15174  infcvgaux1i  15950  infcvgaux2i  15951  cnmsgnsubg  21796  evth2  25194  ivth2  25689  mbfinf  25899  mbfi1flimlem  25956  i1fibl  26042  ditgex  26086  dvrec  26189  dvmptsub  26201  dvexp3  26212  rolle  26224  dvlipcn  26228  dvivth  26244  lhop2  26249  dvfsumge  26256  ftc2  26278  plyremlem  26541  advlogexp  26900  logtayl  26905  logccv  26908  dvatan  27180  amgmlem  27234  emcllem7  27246  basellem9  27333  addsqnreup  27687  axlowdimlem7  29413  axlowdimlem8  29414  axlowdimlem9  29415  axlowdimlem13  29419  sgnsval  33609  sgnsf  33610  xrge0iifcv  34452  xrge0iifiso  34453  xrge0iifhom  34455  dvtan  38427  ftc1anclem5  38454  ftc1anclem6  38455  ftc2nc  38459  areacirclem1  38465  readvrec  43245  monotoddzzfi  43791  monotoddzz  43792  oddcomabszz  43793  rngunsnply  44018  infnsuprnmpt  46087  liminfltlem  46640  dvcosax  46762  itgsin0pilem1  46786  fourierdlem41  46984  fourierdlem48  46990  fourierdlem102  47044  fourierdlem114  47056  fourierswlem  47066  hoicvr  47384  hoicvrrex  47392  smfliminflem  47666  zlmodzxzldeplem3  49440  crosspaltd  50807  amgmwlem  50828