Theorem negex 11390

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  0cc0 11038   − cmin 11376  -cneg 11377

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-nul 5253

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-sn 4583  df-pr 4585  df-uni 4866  df-iota 6456  df-fv 6508  df-ov 7371  df-neg 11379

This theorem is referenced by:  negiso  12134  infrenegsup  12137  xnegex  13135  ceilval  13770  monoord2  13968  m1expcl2  14020  sgnval  15023  infcvgaux1i  15792  infcvgaux2i  15793  cnmsgnsubg  21544  evth2  24927  ivth2  25424  mbfinf  25634  mbfi1flimlem  25691  i1fibl  25777  ditgex  25821  dvrec  25927  dvmptsub  25939  dvexp3  25950  rolle  25962  dvlipcn  25967  dvivth  25983  lhop2  25988  dvfsumge  25996  ftc2  26019  plyremlem  26280  advlogexp  26632  logtayl  26637  logccv  26640  dvatan  26913  amgmlem  26968  emcllem7  26980  basellem9  27067  addsqnreup  27422  axlowdimlem7  29033  axlowdimlem8  29034  axlowdimlem9  29035  axlowdimlem13  29039  sgncl  32922  sgnsval  33254  sgnsf  33255  xrge0iifcv  34111  xrge0iifiso  34112  xrge0iifhom  34114  dvtan  37915  ftc1anclem5  37942  ftc1anclem6  37943  ftc2nc  37947  areacirclem1  37953  readvrec  42726  monotoddzzfi  43293  monotoddzz  43294  oddcomabszz  43295  rngunsnply  43520  infnsuprnmpt  45602  liminfltlem  46156  dvcosax  46278  itgsin0pilem1  46302  fourierdlem41  46500  fourierdlem48  46506  fourierdlem102  46560  fourierdlem114  46572  fourierswlem  46582  hoicvr  46900  hoicvrrex  46908  smfliminflem  47182  zlmodzxzldeplem3  48856  amgmwlem  50155