Theorem negex 11506

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  0cc0 11155   − cmin 11492  -cneg 11493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-nul 5306

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-sn 4627  df-pr 4629  df-uni 4908  df-iota 6514  df-fv 6569  df-ov 7434  df-neg 11495

This theorem is referenced by:  negiso  12248  infrenegsup  12251  xnegex  13250  ceilval  13878  monoord2  14074  m1expcl2  14126  sgnval  15127  infcvgaux1i  15893  infcvgaux2i  15894  cnmsgnsubg  21595  evth2  24992  ivth2  25490  mbfinf  25700  mbfi1flimlem  25757  i1fibl  25843  ditgex  25887  dvrec  25993  dvmptsub  26005  dvexp3  26016  rolle  26028  dvlipcn  26033  dvivth  26049  lhop2  26054  dvfsumge  26062  ftc2  26085  plyremlem  26346  advlogexp  26697  logtayl  26702  logccv  26705  dvatan  26978  amgmlem  27033  emcllem7  27045  basellem9  27132  addsqnreup  27487  axlowdimlem7  28963  axlowdimlem8  28964  axlowdimlem9  28965  axlowdimlem13  28969  sgnsval  33181  sgnsf  33182  xrge0iifcv  33933  xrge0iifiso  33934  xrge0iifhom  33936  sgncl  34541  dvtan  37677  ftc1anclem5  37704  ftc1anclem6  37705  ftc2nc  37709  areacirclem1  37715  readvrec  42392  monotoddzzfi  42954  monotoddzz  42955  oddcomabszz  42956  rngunsnply  43181  infnsuprnmpt  45257  liminfltlem  45819  dvcosax  45941  itgsin0pilem1  45965  fourierdlem41  46163  fourierdlem48  46169  fourierdlem102  46223  fourierdlem114  46235  fourierswlem  46245  hoicvr  46563  hoicvrrex  46571  smfliminflem  46845  zlmodzxzldeplem3  48419  amgmwlem  49321