Theorem 2ex 12315

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ℂcc 11125  2c2 12293

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185  ax-addcl 11187

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-2 12301

This theorem is referenced by:  fzprval  13600  fztpval  13601  funcnvs3  14931  funcnvs4  14932  wrd3tpop  14965  wrdl3s3  14979  pmtrprfval  19466  m2detleiblem3  22565  m2detleiblem4  22566  ehl2eudis  25372  iblcnlem1  25739  gausslemma2dlem4  27330  2lgslem4  27367  addsqnreup  27404  selberglem1  27506  axlowdimlem4  28870  2wlkdlem4  29856  2pthdlem1  29858  umgrwwlks2on  29885  3wlkdlem4  30089  3wlkdlem5  30090  3pthdlem1  30091  3wlkdlem10  30096  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  eulerpathpr  30167  ex-ima  30369  s3rnOLD  32867  cyc3evpm  33107  prodfzo03  34581  circlevma  34620  circlemethhgt  34621  hgt750lemg  34632  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgt  34641  rabren3dioph  42785  refsum2cnlem1  45009  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  cycl3grtrilem  47906  usgrexmpl1lem  47973  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2nb3  47986  usgrexmpl2trifr  47989  zlmodzxzldeplem3  48426  zlmodzxzldeplem4  48427  fv2prop  48628  rrx2pyel  48640  prelrrx2  48641  prelrrx2b  48642  rrx2pnecoorneor  48643  rrx2xpref1o  48646  rrx2plordisom  48651  ehl2eudisval0  48653  rrx2line  48668  rrx2linest  48670  rrx2linesl  48671  2sphere0  48678  line2ylem  48679  line2  48680  line2x  48682  line2y  48683  itscnhlinecirc02p  48713  inlinecirc02plem  48714