Theorem negex 11534

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  0cc0 11184   − cmin 11520  -cneg 11521

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-nul 5324

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-ne 2947  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-sn 4649  df-pr 4651  df-uni 4932  df-iota 6525  df-fv 6581  df-ov 7451  df-neg 11523

This theorem is referenced by:  negiso  12275  infrenegsup  12278  xnegex  13270  ceilval  13889  monoord2  14084  m1expcl2  14136  sgnval  15137  infcvgaux1i  15905  infcvgaux2i  15906  cnmsgnsubg  21618  evth2  25011  ivth2  25509  mbfinf  25719  mbfi1flimlem  25777  i1fibl  25863  ditgex  25907  dvrec  26013  dvmptsub  26025  dvexp3  26036  rolle  26048  dvlipcn  26053  dvivth  26069  lhop2  26074  dvfsumge  26082  ftc2  26105  plyremlem  26364  advlogexp  26715  logtayl  26720  logccv  26723  dvatan  26996  amgmlem  27051  emcllem7  27063  basellem9  27150  addsqnreup  27505  axlowdimlem7  28981  axlowdimlem8  28982  axlowdimlem9  28983  axlowdimlem13  28987  sgnsval  33154  sgnsf  33155  xrge0iifcv  33880  xrge0iifiso  33881  xrge0iifhom  33883  sgncl  34503  dvtan  37630  ftc1anclem5  37657  ftc1anclem6  37658  ftc2nc  37662  areacirclem1  37668  monotoddzzfi  42899  monotoddzz  42900  oddcomabszz  42901  rngunsnply  43130  infnsuprnmpt  45159  liminfltlem  45725  dvcosax  45847  itgsin0pilem1  45871  fourierdlem41  46069  fourierdlem48  46075  fourierdlem102  46129  fourierdlem114  46141  fourierswlem  46151  hoicvr  46469  hoicvrrex  46477  smfliminflem  46751  zlmodzxzldeplem3  48231  amgmwlem  48896