Theorem negex 11425

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  0cc0 11070   − cmin 11411  -cneg 11412

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-nul 5255

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3455  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-sn 4582  df-pr 4584  df-uni 4865  df-iota 6473  df-fv 6525  df-ov 7395  df-neg 11414

This theorem is referenced by:  negiso  12169  infrenegsup  12172  xnegex  13208  ceilval  13845  monoord2  14043  m1expcl2  14095  sgnval  15098  infcvgaux1i  15870  infcvgaux2i  15871  cnmsgnsubg  21609  evth2  25002  ivth2  25497  mbfinf  25707  mbfi1flimlem  25764  i1fibl  25850  ditgex  25894  dvrec  25997  dvmptsub  26009  dvexp3  26020  rolle  26032  dvlipcn  26036  dvivth  26052  lhop2  26057  dvfsumge  26064  ftc2  26086  plyremlem  26345  advlogexp  26697  logtayl  26702  logccv  26705  dvatan  26977  amgmlem  27031  emcllem7  27043  basellem9  27130  addsqnreup  27484  axlowdimlem7  29095  axlowdimlem8  29096  axlowdimlem9  29097  axlowdimlem13  29101  sgncl  32983  sgnsval  33302  sgnsf  33303  xrge0iifcv  34192  xrge0iifiso  34193  xrge0iifhom  34195  dvtan  38133  ftc1anclem5  38160  ftc1anclem6  38161  ftc2nc  38165  areacirclem1  38171  readvrec  42935  monotoddzzfi  43483  monotoddzz  43484  oddcomabszz  43485  rngunsnply  43710  infnsuprnmpt  45789  liminfltlem  46342  dvcosax  46464  itgsin0pilem1  46488  fourierdlem41  46686  fourierdlem48  46692  fourierdlem102  46746  fourierdlem114  46758  fourierswlem  46768  hoicvr  47086  hoicvrrex  47094  smfliminflem  47368  zlmodzxzldeplem3  49088  amgmwlem  50387