Theorem 2ex 12209

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ℂcc 11011  2c2 12187

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 2115  ax-9 2123  ax-ext 2705  ax-1cn 11071  ax-addcl 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-2 12195

This theorem is referenced by:  fzprval  13487  fztpval  13488  funcnvs3  14823  funcnvs4  14824  wrd3tpop  14857  wrdl3s3  14871  ex-chn1  18545  pmtrprfval  19401  m2detleiblem3  22545  m2detleiblem4  22546  ehl2eudis  25350  iblcnlem1  25717  gausslemma2dlem4  27308  2lgslem4  27345  addsqnreup  27382  selberglem1  27484  axlowdimlem4  28925  2wlkdlem4  29908  2pthdlem1  29910  usgrwwlks2on  29938  umgrwwlks2on  29939  3wlkdlem4  30144  3wlkdlem5  30145  3pthdlem1  30146  3wlkdlem10  30151  upgr3v3e3cycl  30162  upgr4cycl4dv4e  30167  eulerpathpr  30222  ex-ima  30424  s3rnOLD  32934  cyc3evpm  33126  prodfzo03  34637  circlevma  34676  circlemethhgt  34677  hgt750lemg  34688  hgt750lemb  34690  hgt750lema  34691  hgt750leme  34692  tgoldbachgtde  34694  tgoldbachgt  34697  rabren3dioph  42932  refsum2cnlem1  45158  nthrucw  47008  nnsum3primes4  47912  nnsum3primesgbe  47916  nnsum4primesodd  47920  nnsum4primesoddALTV  47921  cycl3grtrilem  48070  usgrexmpl1lem  48145  usgrexmpl1tri  48149  usgrexmpl2lem  48150  usgrexmpl2nb0  48155  usgrexmpl2nb1  48156  usgrexmpl2nb2  48157  usgrexmpl2nb3  48158  usgrexmpl2trifr  48161  pglem  48215  zlmodzxzldeplem3  48627  zlmodzxzldeplem4  48628  fv2prop  48825  rrx2pyel  48837  prelrrx2  48838  prelrrx2b  48839  rrx2pnecoorneor  48840  rrx2xpref1o  48843  rrx2plordisom  48848  ehl2eudisval0  48850  rrx2line  48865  rrx2linest  48867  rrx2linesl  48868  2sphere0  48875  line2ylem  48876  line2  48877  line2x  48879  line2y  48880  itscnhlinecirc02p  48910  inlinecirc02plem  48911