Theorem 2ex 12258

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ℂcc 11036  2c2 12236

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-1cn 11096  ax-addcl 11098

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-2 12244

This theorem is referenced by:  fzprval  13539  fztpval  13540  funcnvs3  14876  funcnvs4  14877  wrd3tpop  14910  wrdl3s3  14924  ex-chn1  18603  pmtrprfval  19462  m2detleiblem3  22594  m2detleiblem4  22595  ehl2eudis  25389  iblcnlem1  25755  gausslemma2dlem4  27332  2lgslem4  27369  addsqnreup  27406  selberglem1  27508  axlowdimlem4  29014  2wlkdlem4  29996  2pthdlem1  29998  usgrwwlks2on  30026  umgrwwlks2on  30027  3wlkdlem4  30232  3wlkdlem5  30233  3pthdlem1  30234  3wlkdlem10  30239  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  eulerpathpr  30310  ex-ima  30512  s3rnOLD  33006  cyc3evpm  33211  prodfzo03  34747  circlevma  34786  circlemethhgt  34787  hgt750lemg  34798  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  rabren3dioph  43243  refsum2cnlem1  45468  nthrucw  47316  nnsum3primes4  48264  nnsum3primesgbe  48268  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  cycl3grtrilem  48422  usgrexmpl1lem  48497  usgrexmpl1tri  48501  usgrexmpl2lem  48502  usgrexmpl2nb0  48507  usgrexmpl2nb1  48508  usgrexmpl2nb2  48509  usgrexmpl2nb3  48510  usgrexmpl2trifr  48513  pglem  48567  zlmodzxzldeplem3  48978  zlmodzxzldeplem4  48979  fv2prop  49176  rrx2pyel  49188  prelrrx2  49189  prelrrx2b  49190  rrx2pnecoorneor  49191  rrx2xpref1o  49194  rrx2plordisom  49199  ehl2eudisval0  49201  rrx2line  49216  rrx2linest  49218  rrx2linesl  49219  2sphere0  49226  line2ylem  49227  line2  49228  line2x  49230  line2y  49231  itscnhlinecirc02p  49261  inlinecirc02plem  49262