Theorem negex 10737

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

Syntax hints:   ∈ wcel 2083  Vcvv 3440  0cc0 10390   − cmin 10723  -cneg 10724

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771  ax-nul 5108

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-mo 2578  df-eu 2614  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-ral 3112  df-rex 3113  df-v 3442  df-sbc 3712  df-dif 3868  df-un 3870  df-in 3872  df-ss 3880  df-nul 4218  df-sn 4479  df-pr 4481  df-uni 4752  df-iota 6196  df-fv 6240  df-ov 7026  df-neg 10726

This theorem is referenced by:  negiso  11475  infrenegsup  11478  xnegex  12455  ceilval  13062  monoord2  13255  m1expcl2  13305  sgnval  14285  infcvgaux1i  15049  infcvgaux2i  15050  cnmsgnsubg  20407  evth2  23251  ivth2  23743  mbfinf  23953  mbfi1flimlem  24010  i1fibl  24095  ditgex  24137  dvrec  24239  dvmptsub  24251  dvexp3  24262  rolle  24274  dvlipcn  24278  dvivth  24294  lhop2  24299  dvfsumge  24306  ftc2  24328  plyremlem  24580  advlogexp  24923  logtayl  24928  logccv  24931  dvatan  25198  amgmlem  25253  emcllem7  25265  basellem9  25352  addsqnreup  25705  axlowdimlem7  26421  axlowdimlem8  26422  axlowdimlem9  26423  axlowdimlem13  26427  sgnsval  30437  sgnsf  30438  xrge0iifcv  30790  xrge0iifiso  30791  xrge0iifhom  30793  sgncl  31409  dvtan  34494  ftc1anclem5  34523  ftc1anclem6  34524  ftc2nc  34528  areacirclem1  34534  monotoddzzfi  39045  monotoddzz  39046  oddcomabszz  39047  rngunsnply  39279  infnsuprnmpt  41084  liminfltlem  41648  dvcosax  41774  itgsin0pilem1  41798  fourierdlem41  41997  fourierdlem48  42003  fourierdlem102  42057  fourierdlem114  42069  fourierswlem  42079  hoicvr  42394  hoicvrrex  42402  smfliminflem  42668  zlmodzxzldeplem3  44059  amgmwlem  44405