Theorem 2ex 12050

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 12048	. 2 ⊢ 2 ∈ ℂ
2	1	elexi 3451	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ℂcc 10869  2c2 12028

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-1cn 10929  ax-addcl 10931

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-2 12036

This theorem is referenced by:  fzprval  13317  fztpval  13318  funcnvs3  14627  funcnvs4  14628  wrd3tpop  14661  wrdl3s3  14677  pmtrprfval  19095  m2detleiblem3  21778  m2detleiblem4  21779  ehl2eudis  24586  iblcnlem1  24952  gausslemma2dlem4  26517  2lgslem4  26554  addsqnreup  26591  selberglem1  26693  axlowdimlem4  27313  2wlkdlem4  28293  2pthdlem1  28295  umgrwwlks2on  28322  3wlkdlem4  28526  3wlkdlem5  28527  3pthdlem1  28528  3wlkdlem10  28533  upgr3v3e3cycl  28544  upgr4cycl4dv4e  28549  eulerpathpr  28604  ex-ima  28806  s3rn  31220  cyc3evpm  31417  prodfzo03  32583  circlevma  32622  circlemethhgt  32623  hgt750lemg  32634  hgt750lemb  32636  hgt750lema  32637  hgt750leme  32638  tgoldbachgtde  32640  tgoldbachgt  32643  rabren3dioph  40637  refsum2cnlem1  42580  nnsum3primes4  45240  nnsum3primesgbe  45244  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  zlmodzxzldeplem3  45843  zlmodzxzldeplem4  45844  fv2prop  46046  rrx2pyel  46058  prelrrx2  46059  prelrrx2b  46060  rrx2pnecoorneor  46061  rrx2xpref1o  46064  rrx2plordisom  46069  ehl2eudisval0  46071  rrx2line  46086  rrx2linest  46088  rrx2linesl  46089  2sphere0  46096  line2ylem  46097  line2  46098  line2x  46100  line2y  46101  itscnhlinecirc02p  46131  inlinecirc02plem  46132