Theorem negex 11536

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  0cc0 11181   − cmin 11522  -cneg 11523

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-nul 5260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-sn 4585  df-pr 4587  df-uni 4868  df-iota 6487  df-fv 6539  df-ov 7415  df-neg 11525

This theorem is used by:  negiso  12278  infrenegsup  12281  xnegex  13319  ceilval  13958  monoord2  14156  m1expcl2  14208  sgnval  15221  sgndm  15229  sgncl  15230  infcvgaux1i  16006  infcvgaux2i  16007  cnmsgnsubg  21863  evth2  25261  ivth2  25756  mbfinf  25966  mbfi1flimlem  26023  i1fibl  26108  ditgex  26152  dvrec  26255  dvmptsub  26267  dvexp3  26278  rolle  26290  dvlipcn  26294  dvivth  26310  lhop2  26315  dvfsumge  26322  ftc2  26344  plyremlem  26607  advlogexp  26965  logtayl  26970  logccv  26973  dvatan  27245  amgmlem  27299  emcllem7  27311  basellem9  27398  addsqnreup  27752  axlowdimlem7  29508  axlowdimlem8  29509  axlowdimlem9  29510  axlowdimlem13  29514  sgnsval  33704  sgnsf  33705  xrge0iifcv  34548  xrge0iifiso  34549  xrge0iifhom  34551  dvtan  38556  ftc1anclem5  38583  ftc1anclem6  38584  ftc2nc  38588  areacirclem1  38594  readvrec  43381  monotoddzzfi  43902  monotoddzz  43903  oddcomabszz  43904  rngunsnply  44129  infnsuprnmpt  46205  liminfltlem  46758  dvcosax  46880  itgsin0pilem1  46904  fourierdlem41  47102  fourierdlem48  47108  fourierdlem102  47162  fourierdlem114  47174  fourierswlem  47184  hoicvr  47502  hoicvrrex  47510  smfliminflem  47784  zlmodzxzldeplem3  49558  crosspaltd  50910  amgmwlem  50931