Theorem negex 11456

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  0cc0 11101   − cmin 11442  -cneg 11443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-nul 5270

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-sn 4591  df-pr 4593  df-uni 4874  df-iota 6494  df-fv 6546  df-ov 7415  df-neg 11445

This theorem is referenced by:  negiso  12196  infrenegsup  12199  xnegex  13235  ceilval  13873  monoord2  14071  m1expcl2  14123  sgnval  15127  sgndm  15135  sgncl  15136  infcvgaux1i  15913  infcvgaux2i  15914  cnmsgnsubg  21708  evth2  25100  ivth2  25595  mbfinf  25805  mbfi1flimlem  25862  i1fibl  25948  ditgex  25992  dvrec  26095  dvmptsub  26107  dvexp3  26118  rolle  26130  dvlipcn  26134  dvivth  26150  lhop2  26155  dvfsumge  26162  ftc2  26184  plyremlem  26446  advlogexp  26801  logtayl  26806  logccv  26809  dvatan  27081  amgmlem  27135  emcllem7  27147  basellem9  27234  addsqnreup  27588  axlowdimlem7  29279  axlowdimlem8  29280  axlowdimlem9  29281  axlowdimlem13  29285  sgnsval  33462  sgnsf  33463  xrge0iifcv  34305  xrge0iifiso  34306  xrge0iifhom  34308  dvtan  38302  ftc1anclem5  38329  ftc1anclem6  38330  ftc2nc  38334  areacirclem1  38340  readvrec  43104  monotoddzzfi  43652  monotoddzz  43653  oddcomabszz  43654  rngunsnply  43879  infnsuprnmpt  45948  liminfltlem  46501  dvcosax  46623  itgsin0pilem1  46647  fourierdlem41  46845  fourierdlem48  46851  fourierdlem102  46905  fourierdlem114  46917  fourierswlem  46927  hoicvr  47245  hoicvrrex  47253  smfliminflem  47527  zlmodzxzldeplem3  49265  amgmwlem  50585