Theorem 2ex 12319

Description: The number 2 is a set. (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2ex	⊢ 2 ∈ V

Proof of Theorem 2ex

Step	Hyp	Ref	Expression
1		2cn 12317	. 2 ⊢ 2 ∈ ℂ
2	1	elexi 3484	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 2098  Vcvv 3463  ℂcc 11136  2c2 12297

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-1cn 11196  ax-addcl 11198

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3465  df-2 12305

This theorem is referenced by:  fzprval  13594  fztpval  13595  funcnvs3  14897  funcnvs4  14898  wrd3tpop  14931  wrdl3s3  14945  pmtrprfval  19446  m2detleiblem3  22561  m2detleiblem4  22562  ehl2eudis  25380  iblcnlem1  25747  gausslemma2dlem4  27332  2lgslem4  27369  addsqnreup  27406  selberglem1  27508  axlowdimlem4  28812  2wlkdlem4  29795  2pthdlem1  29797  umgrwwlks2on  29824  3wlkdlem4  30028  3wlkdlem5  30029  3pthdlem1  30030  3wlkdlem10  30035  upgr3v3e3cycl  30046  upgr4cycl4dv4e  30051  eulerpathpr  30106  ex-ima  30308  s3rn  32726  cyc3evpm  32928  prodfzo03  34305  circlevma  34344  circlemethhgt  34345  hgt750lemg  34356  hgt750lemb  34358  hgt750lema  34359  hgt750leme  34360  tgoldbachgtde  34362  tgoldbachgt  34365  rabren3dioph  42300  refsum2cnlem1  44464  nnsum3primes4  47191  nnsum3primesgbe  47195  nnsum4primesodd  47199  nnsum4primesoddALTV  47200  zlmodzxzldeplem3  47682  zlmodzxzldeplem4  47683  fv2prop  47885  rrx2pyel  47897  prelrrx2  47898  prelrrx2b  47899  rrx2pnecoorneor  47900  rrx2xpref1o  47903  rrx2plordisom  47908  ehl2eudisval0  47910  rrx2line  47925  rrx2linest  47927  rrx2linesl  47928  2sphere0  47935  line2ylem  47936  line2  47937  line2x  47939  line2y  47940  itscnhlinecirc02p  47970  inlinecirc02plem  47971