Theorem 2ex 12199

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 11001  2c2 12177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-1cn 11061  ax-addcl 11063

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-2 12185

This theorem is referenced by:  fzprval  13482  fztpval  13483  funcnvs3  14818  funcnvs4  14819  wrd3tpop  14852  wrdl3s3  14866  ex-chn1  18540  pmtrprfval  19397  m2detleiblem3  22542  m2detleiblem4  22543  ehl2eudis  25347  iblcnlem1  25714  gausslemma2dlem4  27305  2lgslem4  27342  addsqnreup  27379  selberglem1  27481  axlowdimlem4  28921  2wlkdlem4  29904  2pthdlem1  29906  umgrwwlks2on  29933  3wlkdlem4  30137  3wlkdlem5  30138  3pthdlem1  30139  3wlkdlem10  30144  upgr3v3e3cycl  30155  upgr4cycl4dv4e  30160  eulerpathpr  30215  ex-ima  30417  s3rnOLD  32922  cyc3evpm  33114  prodfzo03  34611  circlevma  34650  circlemethhgt  34651  hgt750lemg  34662  hgt750lemb  34664  hgt750lema  34665  hgt750leme  34666  tgoldbachgtde  34668  tgoldbachgt  34671  rabren3dioph  42847  refsum2cnlem1  45073  nnsum3primes4  47818  nnsum3primesgbe  47822  nnsum4primesodd  47826  nnsum4primesoddALTV  47827  cycl3grtrilem  47976  usgrexmpl1lem  48051  usgrexmpl1tri  48055  usgrexmpl2lem  48056  usgrexmpl2nb0  48061  usgrexmpl2nb1  48062  usgrexmpl2nb2  48063  usgrexmpl2nb3  48064  usgrexmpl2trifr  48067  pglem  48121  zlmodzxzldeplem3  48533  zlmodzxzldeplem4  48534  fv2prop  48731  rrx2pyel  48743  prelrrx2  48744  prelrrx2b  48745  rrx2pnecoorneor  48746  rrx2xpref1o  48749  rrx2plordisom  48754  ehl2eudisval0  48756  rrx2line  48771  rrx2linest  48773  rrx2linesl  48774  2sphere0  48781  line2ylem  48782  line2  48783  line2x  48785  line2y  48786  itscnhlinecirc02p  48816  inlinecirc02plem  48817