Theorem negex 10158

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 10148	. 2 ⊢ -𝐴 = (0 − 𝐴)
2		ovex 6577	. 2 ⊢ (0 − 𝐴) ∈ V
3	1, 2	eqeltri 2684	1 ⊢ -𝐴 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  (class class class)co 6549  0cc0 9815   − cmin 10145  -cneg 10146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-sn 4126  df-pr 4128  df-uni 4373  df-iota 5768  df-fv 5812  df-ov 6552  df-neg 10148

This theorem is referenced by:  negiso  10880  infrenegsup  10883  xnegex  11913  ceilval  12501  monoord2  12694  m1expcl2  12744  sgnval  13676  infcvgaux1i  14428  infcvgaux2i  14429  cnmsgnsubg  19742  evth2  22567  ivth2  23031  mbfinf  23238  mbfi1flimlem  23295  i1fibl  23380  ditgex  23422  dvrec  23524  dvmptsub  23536  dvexp3  23545  rolle  23557  dvlipcn  23561  dvivth  23577  lhop2  23582  dvfsumge  23589  ftc2  23611  plyremlem  23863  advlogexp  24201  logtayl  24206  logccv  24209  dvatan  24462  amgmlem  24516  emcllem7  24528  basellem9  24615  axlowdimlem7  25628  axlowdimlem8  25629  axlowdimlem9  25630  axlowdimlem13  25634  sgnsval  29059  sgnsf  29060  xrge0iifcv  29308  xrge0iifiso  29309  xrge0iifhom  29311  sgncl  29927  dvtan  32630  ftc1anclem5  32659  ftc1anclem6  32660  ftc2nc  32664  areacirclem1  32670  monotoddzzfi  36525  monotoddzz  36526  oddcomabszz  36527  rngunsnply  36762  dvcosax  38816  itgsin0pilem1  38841  fourierdlem41  39041  fourierdlem48  39047  fourierdlem102  39101  fourierdlem114  39113  fourierswlem  39123  hoicvr  39438  hoicvrrex  39446  zlmodzxzldeplem3  42085  amgmwlem  42357