Theorem negex 11358

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  0cc0 11006   − cmin 11344  -cneg 11345

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 5242

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 3900  df-un 3902  df-ss 3914  df-nul 4281  df-sn 4574  df-pr 4576  df-uni 4857  df-iota 6437  df-fv 6489  df-ov 7349  df-neg 11347

This theorem is referenced by:  negiso  12102  infrenegsup  12105  xnegex  13107  ceilval  13742  monoord2  13940  m1expcl2  13992  sgnval  14995  infcvgaux1i  15764  infcvgaux2i  15765  cnmsgnsubg  21514  evth2  24886  ivth2  25383  mbfinf  25593  mbfi1flimlem  25650  i1fibl  25736  ditgex  25780  dvrec  25886  dvmptsub  25898  dvexp3  25909  rolle  25921  dvlipcn  25926  dvivth  25942  lhop2  25947  dvfsumge  25955  ftc2  25978  plyremlem  26239  advlogexp  26591  logtayl  26596  logccv  26599  dvatan  26872  amgmlem  26927  emcllem7  26939  basellem9  27026  addsqnreup  27381  axlowdimlem7  28926  axlowdimlem8  28927  axlowdimlem9  28928  axlowdimlem13  28932  sgncl  32814  sgnsval  33130  sgnsf  33131  xrge0iifcv  33947  xrge0iifiso  33948  xrge0iifhom  33950  dvtan  37709  ftc1anclem5  37736  ftc1anclem6  37737  ftc2nc  37741  areacirclem1  37747  readvrec  42454  monotoddzzfi  43034  monotoddzz  43035  oddcomabszz  43036  rngunsnply  43261  infnsuprnmpt  45346  liminfltlem  45901  dvcosax  46023  itgsin0pilem1  46047  fourierdlem41  46245  fourierdlem48  46251  fourierdlem102  46305  fourierdlem114  46317  fourierswlem  46327  hoicvr  46645  hoicvrrex  46653  smfliminflem  46927  zlmodzxzldeplem3  48602  amgmwlem  49902