Theorem negex 11473

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  0cc0 11118   − cmin 11459  -cneg 11460

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 2148  ax-9 2156  ax-ext 2738  ax-nul 5274

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 2745  df-cleq 2758  df-clel 2841  df-ne 2962  df-v 3460  df-dif 3911  df-un 3913  df-ss 3925  df-nul 4290  df-sn 4595  df-pr 4597  df-uni 4878  df-iota 6499  df-fv 6551  df-ov 7426  df-neg 11462

This theorem is used by:  negiso  12213  infrenegsup  12216  xnegex  13252  ceilval  13891  monoord2  14089  m1expcl2  14141  sgnval  15151  sgndm  15159  sgncl  15160  infcvgaux1i  15937  infcvgaux2i  15938  cnmsgnsubg  21764  evth2  25156  ivth2  25651  mbfinf  25861  mbfi1flimlem  25918  i1fibl  26004  ditgex  26048  dvrec  26151  dvmptsub  26163  dvexp3  26174  rolle  26186  dvlipcn  26190  dvivth  26206  lhop2  26211  dvfsumge  26218  ftc2  26240  plyremlem  26502  advlogexp  26857  logtayl  26862  logccv  26865  dvatan  27137  amgmlem  27191  emcllem7  27203  basellem9  27290  addsqnreup  27644  axlowdimlem7  29335  axlowdimlem8  29336  axlowdimlem9  29337  axlowdimlem13  29341  sgnsval  33512  sgnsf  33513  xrge0iifcv  34355  xrge0iifiso  34356  xrge0iifhom  34358  dvtan  38362  ftc1anclem5  38389  ftc1anclem6  38390  ftc2nc  38394  areacirclem1  38400  readvrec  43164  monotoddzzfi  43710  monotoddzz  43711  oddcomabszz  43712  rngunsnply  43937  infnsuprnmpt  46006  liminfltlem  46559  dvcosax  46681  itgsin0pilem1  46705  fourierdlem41  46903  fourierdlem48  46909  fourierdlem102  46963  fourierdlem114  46975  fourierswlem  46985  hoicvr  47303  hoicvrrex  47311  smfliminflem  47585  zlmodzxzldeplem3  49323  crosspalti  50689  amgmwlem  50691