Theorem negex 10279

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

Syntax hints:   ∈ wcel 1990  Vcvv 3200  0cc0 9936   − cmin 10266  -cneg 10267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-sn 4178  df-pr 4180  df-uni 4437  df-iota 5851  df-fv 5896  df-ov 6653  df-neg 10269

This theorem is referenced by:  negiso  11003  infrenegsup  11006  xnegex  12039  ceilval  12639  monoord2  12832  m1expcl2  12882  sgnval  13828  infcvgaux1i  14589  infcvgaux2i  14590  cnmsgnsubg  19923  evth2  22759  ivth2  23224  mbfinf  23432  mbfi1flimlem  23489  i1fibl  23574  ditgex  23616  dvrec  23718  dvmptsub  23730  dvexp3  23741  rolle  23753  dvlipcn  23757  dvivth  23773  lhop2  23778  dvfsumge  23785  ftc2  23807  plyremlem  24059  advlogexp  24401  logtayl  24406  logccv  24409  dvatan  24662  amgmlem  24716  emcllem7  24728  basellem9  24815  axlowdimlem7  25828  axlowdimlem8  25829  axlowdimlem9  25830  axlowdimlem13  25834  sgnsval  29728  sgnsf  29729  xrge0iifcv  29980  xrge0iifiso  29981  xrge0iifhom  29983  sgncl  30600  dvtan  33460  ftc1anclem5  33489  ftc1anclem6  33490  ftc2nc  33494  areacirclem1  33500  monotoddzzfi  37507  monotoddzz  37508  oddcomabszz  37509  rngunsnply  37743  infnsuprnmpt  39465  liminfltlem  40036  dvcosax  40141  itgsin0pilem1  40165  fourierdlem41  40365  fourierdlem48  40371  fourierdlem102  40425  fourierdlem114  40437  fourierswlem  40447  hoicvr  40762  hoicvrrex  40770  smfliminflem  41036  zlmodzxzldeplem3  42291  amgmwlem  42548