Theorem negex 11365

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  0cc0 11013   − cmin 11351  -cneg 11352

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-nul 5246

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-sn 4576  df-pr 4578  df-uni 4859  df-iota 6442  df-fv 6494  df-ov 7355  df-neg 11354

This theorem is referenced by:  negiso  12109  infrenegsup  12112  xnegex  13109  ceilval  13744  monoord2  13942  m1expcl2  13994  sgnval  14997  infcvgaux1i  15766  infcvgaux2i  15767  cnmsgnsubg  21516  evth2  24887  ivth2  25384  mbfinf  25594  mbfi1flimlem  25651  i1fibl  25737  ditgex  25781  dvrec  25887  dvmptsub  25899  dvexp3  25910  rolle  25922  dvlipcn  25927  dvivth  25943  lhop2  25948  dvfsumge  25956  ftc2  25979  plyremlem  26240  advlogexp  26592  logtayl  26597  logccv  26600  dvatan  26873  amgmlem  26928  emcllem7  26940  basellem9  27027  addsqnreup  27382  axlowdimlem7  28928  axlowdimlem8  28929  axlowdimlem9  28930  axlowdimlem13  28934  sgncl  32819  sgnsval  33137  sgnsf  33138  xrge0iifcv  33968  xrge0iifiso  33969  xrge0iifhom  33971  dvtan  37730  ftc1anclem5  37757  ftc1anclem6  37758  ftc2nc  37762  areacirclem1  37768  readvrec  42480  monotoddzzfi  43059  monotoddzz  43060  oddcomabszz  43061  rngunsnply  43286  infnsuprnmpt  45371  liminfltlem  45926  dvcosax  46048  itgsin0pilem1  46072  fourierdlem41  46270  fourierdlem48  46276  fourierdlem102  46330  fourierdlem114  46342  fourierswlem  46352  hoicvr  46670  hoicvrrex  46678  smfliminflem  46952  zlmodzxzldeplem3  48627  amgmwlem  49927