Theorem 2ex 12281

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

Syntax hints:   ∈ wcel 2132  Vcvv 3444  ℂcc 11057  2c2 12258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-ext 2724  ax-1cn 11117  ax-addcl 11119

This theorem depends on definitions:  df-bi 209  df-an 399  df-tru 1553  df-ex 1790  df-sb 2081  df-clab 2731  df-cleq 2744  df-clel 2827  df-v 3446  df-2 12266

This theorem is referenced by:  fzprval  13576  fztpval  13577  funcnvs3  14913  funcnvs4  14914  wrd3tpop  14947  wrdl3s3  14961  ex-chn1  18641  pmtrprfval  19499  m2detleiblem3  22658  m2detleiblem4  22659  ehl2eudis  25453  iblcnlem1  25819  gausslemma2dlem4  27399  2lgslem4  27436  addsqnreup  27473  selberglem1  27575  axlowdimlem4  29081  2wlkdlem4  30063  2pthdlem1  30065  usgrwwlks2on  30093  umgrwwlks2on  30094  3wlkdlem4  30299  3wlkdlem5  30300  3pthdlem1  30301  3wlkdlem10  30306  upgr3v3e3cycl  30317  upgr4cycl4dv4e  30322  eulerpathpr  30377  ex-ima  30579  s3rnOLD  33074  cyc3evpm  33280  prodfzo03  34844  circlevma  34883  circlemethhgt  34884  hgt750lemg  34895  hgt750lemb  34897  hgt750lema  34898  hgt750leme  34899  tgoldbachgtde  34901  tgoldbachgt  34904  rabren3dioph  43330  refsum2cnlem1  45555  nthrucw  47400  nnsum3primes4  48348  nnsum3primesgbe  48352  nnsum4primesodd  48356  nnsum4primesoddALTV  48357  cycl3grtrilem  48506  usgrexmpl1lem  48581  usgrexmpl1tri  48585  usgrexmpl2lem  48586  usgrexmpl2nb0  48591  usgrexmpl2nb1  48592  usgrexmpl2nb2  48593  usgrexmpl2nb3  48594  usgrexmpl2trifr  48597  pglem  48651  zlmodzxzldeplem3  49062  zlmodzxzldeplem4  49063  fv2prop  49260  rrx2pyel  49272  prelrrx2  49273  prelrrx2b  49274  rrx2pnecoorneor  49275  rrx2xpref1o  49278  rrx2plordisom  49283  ehl2eudisval0  49285  rrx2line  49300  rrx2linest  49302  rrx2linesl  49303  2sphere0  49310  line2ylem  49311  line2  49312  line2x  49314  line2y  49315  itscnhlinecirc02p  49345  inlinecirc02plem  49346