Theorem negex 11454

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  0cc0 11106   − cmin 11440  -cneg 11441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-nul 5305

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908  df-iota 6492  df-fv 6548  df-ov 7408  df-neg 11443

This theorem is referenced by:  negiso  12190  infrenegsup  12193  xnegex  13183  ceilval  13799  monoord2  13995  m1expcl2  14047  sgnval  15031  infcvgaux1i  15799  infcvgaux2i  15800  cnmsgnsubg  21121  evth2  24467  ivth2  24963  mbfinf  25173  mbfi1flimlem  25231  i1fibl  25316  ditgex  25360  dvrec  25463  dvmptsub  25475  dvexp3  25486  rolle  25498  dvlipcn  25502  dvivth  25518  lhop2  25523  dvfsumge  25530  ftc2  25552  plyremlem  25808  advlogexp  26154  logtayl  26159  logccv  26162  dvatan  26429  amgmlem  26483  emcllem7  26495  basellem9  26582  addsqnreup  26935  axlowdimlem7  28195  axlowdimlem8  28196  axlowdimlem9  28197  axlowdimlem13  28201  sgnsval  32307  sgnsf  32308  xrge0iifcv  32902  xrge0iifiso  32903  xrge0iifhom  32905  sgncl  33525  dvtan  36526  ftc1anclem5  36553  ftc1anclem6  36554  ftc2nc  36558  areacirclem1  36564  monotoddzzfi  41666  monotoddzz  41667  oddcomabszz  41668  rngunsnply  41900  infnsuprnmpt  43940  liminfltlem  44506  dvcosax  44628  itgsin0pilem1  44652  fourierdlem41  44850  fourierdlem48  44856  fourierdlem102  44910  fourierdlem114  44922  fourierswlem  44932  hoicvr  45250  hoicvrrex  45258  smfliminflem  45532  zlmodzxzldeplem3  47136  amgmwlem  47802