Theorem negex 11265

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

Syntax hints:   ∈ wcel 2104  Vcvv 3437  0cc0 10917   − cmin 11251  -cneg 11252

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707  ax-nul 5239

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2942  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-sn 4566  df-pr 4568  df-uni 4845  df-iota 6410  df-fv 6466  df-ov 7310  df-neg 11254

This theorem is referenced by:  negiso  12001  infrenegsup  12004  xnegex  12988  ceilval  13604  monoord2  13800  m1expcl2  13850  sgnval  14844  infcvgaux1i  15614  infcvgaux2i  15615  cnmsgnsubg  20827  evth2  24168  ivth2  24664  mbfinf  24874  mbfi1flimlem  24932  i1fibl  25017  ditgex  25061  dvrec  25164  dvmptsub  25176  dvexp3  25187  rolle  25199  dvlipcn  25203  dvivth  25219  lhop2  25224  dvfsumge  25231  ftc2  25253  plyremlem  25509  advlogexp  25855  logtayl  25860  logccv  25863  dvatan  26130  amgmlem  26184  emcllem7  26196  basellem9  26283  addsqnreup  26636  axlowdimlem7  27361  axlowdimlem8  27362  axlowdimlem9  27363  axlowdimlem13  27367  sgnsval  31473  sgnsf  31474  xrge0iifcv  31929  xrge0iifiso  31930  xrge0iifhom  31932  sgncl  32550  dvtan  35871  ftc1anclem5  35898  ftc1anclem6  35899  ftc2nc  35903  areacirclem1  35909  monotoddzzfi  40802  monotoddzz  40803  oddcomabszz  40804  rngunsnply  41036  infnsuprnmpt  42841  liminfltlem  43394  dvcosax  43516  itgsin0pilem1  43540  fourierdlem41  43738  fourierdlem48  43744  fourierdlem102  43798  fourierdlem114  43810  fourierswlem  43820  hoicvr  44136  hoicvrrex  44144  smfliminflem  44417  zlmodzxzldeplem3  45901  amgmwlem  46564