Theorem negex 11558

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  0cc0 11203   − cmin 11544   -cneg 11545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-v 3452  df-ss 3896  df-dif 4047  df-un 4151  df-nul 4279  df-sn 4585  df-pr 4587  df-uni 4867  df-iota 6494  df-fv 6546  df-ov 7423  df-neg 11547

This theorem is used by:  negiso  12300  infrenegsup  12303  xnegex  13341  ceilval  13981  monoord2  14179  m1expcl2  14231  sgnval  15246  sgndm  15254  sgncl  15255  infcvgaux1i  16031  infcvgaux2i  16032  cnmsgnsubg  21888  evth2  25286  ivth2  25781  mbfinf  25991  mbfi1flimlem  26048  i1fibl  26133  ditgex  26177  dvrec  26280  dvmptsub  26292  dvexp3  26303  rolle  26315  dvlipcn  26319  dvivth  26335  lhop2  26340  dvfsumge  26347  ftc2  26369  plyremlem  26630  advlogexp  26988  logtayl  26993  logccv  26996  dvatan  27268  amgmlem  27322  emcllem7  27334  basellem9  27421  addsqnreup  27775  axlowdimlem7  29531  axlowdimlem8  29532  axlowdimlem9  29533  axlowdimlem13  29537  sgnsval  33768  sgnsf  33769  xrge0iifcv  34612  xrge0iifiso  34613  xrge0iifhom  34615  dvtan  38681  ftc1anclem5  38708  ftc1anclem6  38709  ftc2nc  38713  areacirclem1  38719  readvrec  43506  monotoddzzfi  44042  monotoddzz  44043  oddcomabszz  44044  rngunsnply  44264  infnsuprnmpt  46355  liminfltlem  46907  dvcosax  47029  itgsin0pilem1  47053  fourierdlem41  47251  fourierdlem48  47257  fourierdlem102  47311  fourierdlem114  47323  fourierswlem  47333  hoicvr  47651  hoicvrrex  47659  smfliminflem  47933  zlmodzxzldeplem3  49707  crosspaltd  51134  amgmwlem  51155