Theorem negex 10317

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

Syntax hints:   ∈ wcel 2030  Vcvv 3231  0cc0 9974   − cmin 10304  -cneg 10305

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-nul 4822

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-sn 4211  df-pr 4213  df-uni 4469  df-iota 5889  df-fv 5934  df-ov 6693  df-neg 10307

This theorem is referenced by:  negiso  11041  infrenegsup  11044  xnegex  12077  ceilval  12679  monoord2  12872  m1expcl2  12922  sgnval  13872  infcvgaux1i  14633  infcvgaux2i  14634  cnmsgnsubg  19971  evth2  22806  ivth2  23270  mbfinf  23477  mbfi1flimlem  23534  i1fibl  23619  ditgex  23661  dvrec  23763  dvmptsub  23775  dvexp3  23786  rolle  23798  dvlipcn  23802  dvivth  23818  lhop2  23823  dvfsumge  23830  ftc2  23852  plyremlem  24104  advlogexp  24446  logtayl  24451  logccv  24454  dvatan  24707  amgmlem  24761  emcllem7  24773  basellem9  24860  axlowdimlem7  25873  axlowdimlem8  25874  axlowdimlem9  25875  axlowdimlem13  25879  sgnsval  29856  sgnsf  29857  xrge0iifcv  30108  xrge0iifiso  30109  xrge0iifhom  30111  sgncl  30728  dvtan  33590  ftc1anclem5  33619  ftc1anclem6  33620  ftc2nc  33624  areacirclem1  33630  monotoddzzfi  37824  monotoddzz  37825  oddcomabszz  37826  rngunsnply  38060  infnsuprnmpt  39779  liminfltlem  40354  dvcosax  40459  itgsin0pilem1  40483  fourierdlem41  40683  fourierdlem48  40689  fourierdlem102  40743  fourierdlem114  40755  fourierswlem  40765  hoicvr  41083  hoicvrrex  41091  smfliminflem  41357  zlmodzxzldeplem3  42616  amgmwlem  42876