Theorem negex 11445

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  0cc0 11097   − cmin 11431  -cneg 11432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5302

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-v 3477  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-nul 4321  df-sn 4625  df-pr 4627  df-uni 4905  df-iota 6487  df-fv 6543  df-ov 7399  df-neg 11434

This theorem is referenced by:  negiso  12181  infrenegsup  12184  xnegex  13174  ceilval  13790  monoord2  13986  m1expcl2  14038  sgnval  15022  infcvgaux1i  15790  infcvgaux2i  15791  cnmsgnsubg  21103  evth2  24445  ivth2  24941  mbfinf  25151  mbfi1flimlem  25209  i1fibl  25294  ditgex  25338  dvrec  25441  dvmptsub  25453  dvexp3  25464  rolle  25476  dvlipcn  25480  dvivth  25496  lhop2  25501  dvfsumge  25508  ftc2  25530  plyremlem  25786  advlogexp  26132  logtayl  26137  logccv  26140  dvatan  26407  amgmlem  26461  emcllem7  26473  basellem9  26560  addsqnreup  26913  axlowdimlem7  28173  axlowdimlem8  28174  axlowdimlem9  28175  axlowdimlem13  28179  sgnsval  32291  sgnsf  32292  xrge0iifcv  32845  xrge0iifiso  32846  xrge0iifhom  32848  sgncl  33468  dvtan  36443  ftc1anclem5  36470  ftc1anclem6  36471  ftc2nc  36475  areacirclem1  36481  monotoddzzfi  41552  monotoddzz  41553  oddcomabszz  41554  rngunsnply  41786  infnsuprnmpt  43827  liminfltlem  44393  dvcosax  44515  itgsin0pilem1  44539  fourierdlem41  44737  fourierdlem48  44743  fourierdlem102  44797  fourierdlem114  44809  fourierswlem  44819  hoicvr  45137  hoicvrrex  45145  smfliminflem  45419  zlmodzxzldeplem3  47023  amgmwlem  47689