Theorem negex 11426

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  0cc0 11075   − cmin 11412  -cneg 11413

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-nul 5264

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875  df-iota 6467  df-fv 6522  df-ov 7393  df-neg 11415

This theorem is referenced by:  negiso  12170  infrenegsup  12173  xnegex  13175  ceilval  13807  monoord2  14005  m1expcl2  14057  sgnval  15061  infcvgaux1i  15830  infcvgaux2i  15831  cnmsgnsubg  21493  evth2  24866  ivth2  25363  mbfinf  25573  mbfi1flimlem  25630  i1fibl  25716  ditgex  25760  dvrec  25866  dvmptsub  25878  dvexp3  25889  rolle  25901  dvlipcn  25906  dvivth  25922  lhop2  25927  dvfsumge  25935  ftc2  25958  plyremlem  26219  advlogexp  26571  logtayl  26576  logccv  26579  dvatan  26852  amgmlem  26907  emcllem7  26919  basellem9  27006  addsqnreup  27361  axlowdimlem7  28882  axlowdimlem8  28883  axlowdimlem9  28884  axlowdimlem13  28888  sgncl  32763  sgnsval  33125  sgnsf  33126  xrge0iifcv  33931  xrge0iifiso  33932  xrge0iifhom  33934  dvtan  37671  ftc1anclem5  37698  ftc1anclem6  37699  ftc2nc  37703  areacirclem1  37709  readvrec  42357  monotoddzzfi  42938  monotoddzz  42939  oddcomabszz  42940  rngunsnply  43165  infnsuprnmpt  45251  liminfltlem  45809  dvcosax  45931  itgsin0pilem1  45955  fourierdlem41  46153  fourierdlem48  46159  fourierdlem102  46213  fourierdlem114  46225  fourierswlem  46235  hoicvr  46553  hoicvrrex  46561  smfliminflem  46835  zlmodzxzldeplem3  48495  amgmwlem  49795