Theorem 2ex 12401

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11179  2c2 12378

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11239  ax-addcl 11241

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-2 12386

This theorem is used by:  fzprval  13699  fztpval  13700  funcnvs3  15045  funcnvs4  15046  wrd3tpop  15079  s3rex  15081  wrdl3s3  15095  ex-chn1  18791  pmtrprfval  19681  m2detleiblem3  22924  m2detleiblem4  22925  ehl2eudis  25723  iblcnlem1  26088  gausslemma2dlem4  27678  2lgslem4  27715  addsqnreup  27752  selberglem1  27854  elcgrabasi  29357  axlowdimlem4  29505  2wlkdlem4  30499  2pthdlem1  30501  usgrwwlks2on  30529  umgrwwlks2on  30530  3wlkdlem4  30745  3wlkdlem5  30746  3pthdlem1  30747  3wlkdlem10  30752  upgr3v3e3cycl  30763  upgr4cycl4dv4e  30768  eulerpathpr  30823  ex-ima  31025  cyc3evpm  33693  prodfzo03  35215  circlevma  35254  circlemethhgt  35255  hgt750lemg  35266  hgt750lemb  35268  hgt750lema  35269  hgt750leme  35270  tgoldbachgtde  35272  tgoldbachgt  35275  rabren3dioph  43775  refsum2cnlem1  45997  nnsum3primes4  48830  nnsum3primesgbe  48834  nnsum4primesodd  48838  nnsum4primesoddALTV  48839  cycl3grtrilem  48988  usgrexmpl1lem  49063  usgrexmpl1tri  49067  usgrexmpl2lem  49068  usgrexmpl2nb0  49073  usgrexmpl2nb1  49074  usgrexmpl2nb2  49075  usgrexmpl2nb3  49076  usgrexmpl2trifr  49079  pglem  49133  zlmodzxzldeplem3  49558  zlmodzxzldeplem4  49559  fv2prop  49756  rrx2pyel  49768  prelrrx2  49769  prelrrx2b  49770  rrx2pnecoorneor  49771  rrx2xpref1o  49774  rrx2plordisom  49779  ehl2eudisval0  49781  rrx2line  49796  rrx2linest  49798  rrx2linesl  49799  2sphere0  49806  line2ylem  49807  line2  49808  line2x  49810  line2y  49811  itscnhlinecirc02p  49841  inlinecirc02plem  49842