Theorem 2ex 12234

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂcc 11036  2c2 12212

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 2709  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 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-2 12220

This theorem is referenced by:  fzprval  13513  fztpval  13514  funcnvs3  14849  funcnvs4  14850  wrd3tpop  14883  wrdl3s3  14897  ex-chn1  18572  pmtrprfval  19428  m2detleiblem3  22585  m2detleiblem4  22586  ehl2eudis  25390  iblcnlem1  25757  gausslemma2dlem4  27348  2lgslem4  27385  addsqnreup  27422  selberglem1  27524  axlowdimlem4  29030  2wlkdlem4  30013  2pthdlem1  30015  usgrwwlks2on  30043  umgrwwlks2on  30044  3wlkdlem4  30249  3wlkdlem5  30250  3pthdlem1  30251  3wlkdlem10  30256  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  eulerpathpr  30327  ex-ima  30529  s3rnOLD  33038  cyc3evpm  33243  prodfzo03  34780  circlevma  34819  circlemethhgt  34820  hgt750lemg  34831  hgt750lemb  34833  hgt750lema  34834  hgt750leme  34835  tgoldbachgtde  34837  tgoldbachgt  34840  rabren3dioph  43166  refsum2cnlem1  45391  nthrucw  47238  nnsum3primes4  48142  nnsum3primesgbe  48146  nnsum4primesodd  48150  nnsum4primesoddALTV  48151  cycl3grtrilem  48300  usgrexmpl1lem  48375  usgrexmpl1tri  48379  usgrexmpl2lem  48380  usgrexmpl2nb0  48385  usgrexmpl2nb1  48386  usgrexmpl2nb2  48387  usgrexmpl2nb3  48388  usgrexmpl2trifr  48391  pglem  48445  zlmodzxzldeplem3  48856  zlmodzxzldeplem4  48857  fv2prop  49054  rrx2pyel  49066  prelrrx2  49067  prelrrx2b  49068  rrx2pnecoorneor  49069  rrx2xpref1o  49072  rrx2plordisom  49077  ehl2eudisval0  49079  rrx2line  49094  rrx2linest  49096  rrx2linesl  49097  2sphere0  49104  line2ylem  49105  line2  49106  line2x  49108  line2y  49109  itscnhlinecirc02p  49139  inlinecirc02plem  49140