Theorem negex 11389

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  0cc0 11036   − cmin 11375  -cneg 11376

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-sn 4563  df-pr 4565  df-uni 4846  df-iota 6448  df-fv 6500  df-ov 7366  df-neg 11378

This theorem is referenced by:  negiso  12134  infrenegsup  12137  xnegex  13158  ceilval  13795  monoord2  13993  m1expcl2  14045  sgnval  15048  infcvgaux1i  15820  infcvgaux2i  15821  cnmsgnsubg  21559  evth2  24952  ivth2  25447  mbfinf  25657  mbfi1flimlem  25714  i1fibl  25800  ditgex  25844  dvrec  25947  dvmptsub  25959  dvexp3  25970  rolle  25982  dvlipcn  25986  dvivth  26002  lhop2  26007  dvfsumge  26014  ftc2  26036  plyremlem  26295  advlogexp  26644  logtayl  26649  logccv  26652  dvatan  26924  amgmlem  26978  emcllem7  26990  basellem9  27077  addsqnreup  27431  axlowdimlem7  29042  axlowdimlem8  29043  axlowdimlem9  29044  axlowdimlem13  29048  sgncl  32930  sgnsval  33249  sgnsf  33250  xrge0iifcv  34125  xrge0iifiso  34126  xrge0iifhom  34128  dvtan  38044  ftc1anclem5  38071  ftc1anclem6  38072  ftc2nc  38076  areacirclem1  38082  readvrec  42846  monotoddzzfi  43394  monotoddzz  43395  oddcomabszz  43396  rngunsnply  43621  infnsuprnmpt  45701  liminfltlem  46254  dvcosax  46376  itgsin0pilem1  46400  fourierdlem41  46598  fourierdlem48  46604  fourierdlem102  46658  fourierdlem114  46670  fourierswlem  46680  hoicvr  46998  hoicvrrex  47006  smfliminflem  47280  zlmodzxzldeplem3  49000  amgmwlem  50299