Theorem negex 11355

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  0cc0 11003   − cmin 11341  -cneg 11342

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-nul 5244

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-sn 4577  df-pr 4579  df-uni 4860  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11344

This theorem is referenced by:  negiso  12099  infrenegsup  12102  xnegex  13104  ceilval  13739  monoord2  13937  m1expcl2  13989  sgnval  14992  infcvgaux1i  15761  infcvgaux2i  15762  cnmsgnsubg  21512  evth2  24884  ivth2  25381  mbfinf  25591  mbfi1flimlem  25648  i1fibl  25734  ditgex  25778  dvrec  25884  dvmptsub  25896  dvexp3  25907  rolle  25919  dvlipcn  25924  dvivth  25940  lhop2  25945  dvfsumge  25953  ftc2  25976  plyremlem  26237  advlogexp  26589  logtayl  26594  logccv  26597  dvatan  26870  amgmlem  26925  emcllem7  26937  basellem9  27024  addsqnreup  27379  axlowdimlem7  28924  axlowdimlem8  28925  axlowdimlem9  28926  axlowdimlem13  28930  sgncl  32809  sgnsval  33125  sgnsf  33126  xrge0iifcv  33942  xrge0iifiso  33943  xrge0iifhom  33945  dvtan  37709  ftc1anclem5  37736  ftc1anclem6  37737  ftc2nc  37741  areacirclem1  37747  readvrec  42394  monotoddzzfi  42974  monotoddzz  42975  oddcomabszz  42976  rngunsnply  43201  infnsuprnmpt  45286  liminfltlem  45841  dvcosax  45963  itgsin0pilem1  45987  fourierdlem41  46185  fourierdlem48  46191  fourierdlem102  46245  fourierdlem114  46257  fourierswlem  46267  hoicvr  46585  hoicvrrex  46593  smfliminflem  46867  zlmodzxzldeplem3  48533  amgmwlem  49833