Theorem negex 10887

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

Syntax hints:   ∈ wcel 2113  Vcvv 3497  0cc0 10540   − cmin 10873  -cneg 10874

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-nul 5213

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ral 3146  df-rex 3147  df-v 3499  df-sbc 3776  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-sn 4571  df-pr 4573  df-uni 4842  df-iota 6317  df-fv 6366  df-ov 7162  df-neg 10876

This theorem is referenced by:  negiso  11624  infrenegsup  11627  xnegex  12604  ceilval  13211  monoord2  13404  m1expcl2  13454  sgnval  14450  infcvgaux1i  15215  infcvgaux2i  15216  cnmsgnsubg  20724  evth2  23567  ivth2  24059  mbfinf  24269  mbfi1flimlem  24326  i1fibl  24411  ditgex  24453  dvrec  24555  dvmptsub  24567  dvexp3  24578  rolle  24590  dvlipcn  24594  dvivth  24610  lhop2  24615  dvfsumge  24622  ftc2  24644  plyremlem  24896  advlogexp  25241  logtayl  25246  logccv  25249  dvatan  25516  amgmlem  25570  emcllem7  25582  basellem9  25669  addsqnreup  26022  axlowdimlem7  26737  axlowdimlem8  26738  axlowdimlem9  26739  axlowdimlem13  26743  sgnsval  30807  sgnsf  30808  xrge0iifcv  31181  xrge0iifiso  31182  xrge0iifhom  31184  sgncl  31800  dvtan  34946  ftc1anclem5  34975  ftc1anclem6  34976  ftc2nc  34980  areacirclem1  34986  monotoddzzfi  39545  monotoddzz  39546  oddcomabszz  39547  rngunsnply  39779  infnsuprnmpt  41528  liminfltlem  42091  dvcosax  42217  itgsin0pilem1  42241  fourierdlem41  42440  fourierdlem48  42446  fourierdlem102  42500  fourierdlem114  42512  fourierswlem  42522  hoicvr  42837  hoicvrrex  42845  smfliminflem  43111  zlmodzxzldeplem3  44564  amgmwlem  44910