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 3477	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ℂcc 11099  2c2 12296

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-1cn 11159  ax-addcl 11161

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-2 12304

This theorem is referenced by:  fzprval  13615  fztpval  13616  funcnvs3  14953  funcnvs4  14954  wrd3tpop  14987  wrdl3s3  15001  ex-chn1  18694  pmtrprfval  19558  m2detleiblem3  22767  m2detleiblem4  22768  ehl2eudis  25562  iblcnlem1  25928  gausslemma2dlem4  27514  2lgslem4  27551  addsqnreup  27588  selberglem1  27690  axlowdimlem4  29276  2wlkdlem4  30258  2pthdlem1  30260  usgrwwlks2on  30288  umgrwwlks2on  30289  3wlkdlem4  30494  3wlkdlem5  30495  3pthdlem1  30496  3wlkdlem10  30501  upgr3v3e3cycl  30512  upgr4cycl4dv4e  30517  eulerpathpr  30572  ex-ima  30774  s3rnOLD  33247  cyc3evpm  33451  prodfzo03  34971  circlevma  35010  circlemethhgt  35011  hgt750lemg  35022  hgt750lemb  35024  hgt750lema  35025  hgt750leme  35026  tgoldbachgtde  35028  tgoldbachgt  35031  rabren3dioph  43525  refsum2cnlem1  45740  nnsum3primes4  48536  nnsum3primesgbe  48540  nnsum4primesodd  48544  nnsum4primesoddALTV  48545  cycl3grtrilem  48694  usgrexmpl1lem  48769  usgrexmpl1tri  48773  usgrexmpl2lem  48774  usgrexmpl2nb0  48779  usgrexmpl2nb1  48780  usgrexmpl2nb2  48781  usgrexmpl2nb3  48782  usgrexmpl2trifr  48785  pglem  48839  zlmodzxzldeplem3  49265  zlmodzxzldeplem4  49266  fv2prop  49463  rrx2pyel  49475  prelrrx2  49476  prelrrx2b  49477  rrx2pnecoorneor  49478  rrx2xpref1o  49481  rrx2plordisom  49486  ehl2eudisval0  49488  rrx2line  49503  rrx2linest  49505  rrx2linesl  49506  2sphere0  49513  line2ylem  49514  line2  49515  line2x  49517  line2y  49518  itscnhlinecirc02p  49548  inlinecirc02plem  49549