Theorem 2ex 12285

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11104  2c2 12263

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164  ax-addcl 11166

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-2 12271

This theorem is referenced by:  fzprval  13558  fztpval  13559  funcnvs3  14861  funcnvs4  14862  wrd3tpop  14895  wrdl3s3  14909  pmtrprfval  19349  m2detleiblem3  22122  m2detleiblem4  22123  ehl2eudis  24930  iblcnlem1  25296  gausslemma2dlem4  26861  2lgslem4  26898  addsqnreup  26935  selberglem1  27037  axlowdimlem4  28192  2wlkdlem4  29171  2pthdlem1  29173  umgrwwlks2on  29200  3wlkdlem4  29404  3wlkdlem5  29405  3pthdlem1  29406  3wlkdlem10  29411  upgr3v3e3cycl  29422  upgr4cycl4dv4e  29427  eulerpathpr  29482  ex-ima  29684  s3rn  32099  cyc3evpm  32296  prodfzo03  33603  circlevma  33642  circlemethhgt  33643  hgt750lemg  33654  hgt750lemb  33656  hgt750lema  33657  hgt750leme  33658  tgoldbachgtde  33660  tgoldbachgt  33663  rabren3dioph  41538  refsum2cnlem1  43706  nnsum3primes4  46442  nnsum3primesgbe  46446  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  zlmodzxzldeplem3  47136  zlmodzxzldeplem4  47137  fv2prop  47339  rrx2pyel  47351  prelrrx2  47352  prelrrx2b  47353  rrx2pnecoorneor  47354  rrx2xpref1o  47357  rrx2plordisom  47362  ehl2eudisval0  47364  rrx2line  47379  rrx2linest  47381  rrx2linesl  47382  2sphere0  47389  line2ylem  47390  line2  47391  line2x  47393  line2y  47394  itscnhlinecirc02p  47424  inlinecirc02plem  47425