Theorem 2ex 12292

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ℂcc 11068  2c2 12269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11128  ax-addcl 11130

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-2 12277

This theorem is referenced by:  fzprval  13587  fztpval  13588  funcnvs3  14924  funcnvs4  14925  wrd3tpop  14958  wrdl3s3  14972  ex-chn1  18652  pmtrprfval  19510  m2detleiblem3  22669  m2detleiblem4  22670  ehl2eudis  25464  iblcnlem1  25830  gausslemma2dlem4  27410  2lgslem4  27447  addsqnreup  27484  selberglem1  27586  axlowdimlem4  29092  2wlkdlem4  30074  2pthdlem1  30076  usgrwwlks2on  30104  umgrwwlks2on  30105  3wlkdlem4  30310  3wlkdlem5  30311  3pthdlem1  30312  3wlkdlem10  30317  upgr3v3e3cycl  30328  upgr4cycl4dv4e  30333  eulerpathpr  30388  ex-ima  30590  s3rnOLD  33085  cyc3evpm  33291  prodfzo03  34861  circlevma  34900  circlemethhgt  34901  hgt750lemg  34912  hgt750lemb  34914  hgt750lema  34915  hgt750leme  34916  tgoldbachgtde  34918  tgoldbachgt  34921  rabren3dioph  43356  refsum2cnlem1  45581  nthrucw  47426  nnsum3primes4  48374  nnsum3primesgbe  48378  nnsum4primesodd  48382  nnsum4primesoddALTV  48383  cycl3grtrilem  48532  usgrexmpl1lem  48607  usgrexmpl1tri  48611  usgrexmpl2lem  48612  usgrexmpl2nb0  48617  usgrexmpl2nb1  48618  usgrexmpl2nb2  48619  usgrexmpl2nb3  48620  usgrexmpl2trifr  48623  pglem  48677  zlmodzxzldeplem3  49088  zlmodzxzldeplem4  49089  fv2prop  49286  rrx2pyel  49298  prelrrx2  49299  prelrrx2b  49300  rrx2pnecoorneor  49301  rrx2xpref1o  49304  rrx2plordisom  49309  ehl2eudisval0  49311  rrx2line  49326  rrx2linest  49328  rrx2linesl  49329  2sphere0  49336  line2ylem  49337  line2  49338  line2x  49340  line2y  49341  itscnhlinecirc02p  49371  inlinecirc02plem  49372