Theorem 2ex 12346

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  ℂcc 11126  2c2 12323

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 2734  ax-1cn 11186  ax-addcl 11188

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-2 12331

This theorem is used by:  fzprval  13644  fztpval  13645  funcnvs3  14989  funcnvs4  14990  wrd3tpop  15023  s3rex  15025  wrdl3s3  15039  ex-chn1  18731  pmtrprfval  19620  m2detleiblem3  22857  m2detleiblem4  22858  ehl2eudis  25656  iblcnlem1  26022  gausslemma2dlem4  27613  2lgslem4  27650  addsqnreup  27687  selberglem1  27789  elcgrabasi  29262  axlowdimlem4  29410  2wlkdlem4  30404  2pthdlem1  30406  usgrwwlks2on  30434  umgrwwlks2on  30435  3wlkdlem4  30650  3wlkdlem5  30651  3pthdlem1  30652  3wlkdlem10  30657  upgr3v3e3cycl  30668  upgr4cycl4dv4e  30673  eulerpathpr  30728  ex-ima  30930  cyc3evpm  33598  prodfzo03  35119  circlevma  35158  circlemethhgt  35159  hgt750lemg  35170  hgt750lemb  35172  hgt750lema  35173  hgt750leme  35174  tgoldbachgtde  35176  tgoldbachgt  35179  rabren3dioph  43664  refsum2cnlem1  45879  nnsum3primes4  48712  nnsum3primesgbe  48716  nnsum4primesodd  48720  nnsum4primesoddALTV  48721  cycl3grtrilem  48870  usgrexmpl1lem  48945  usgrexmpl1tri  48949  usgrexmpl2lem  48950  usgrexmpl2nb0  48955  usgrexmpl2nb1  48956  usgrexmpl2nb2  48957  usgrexmpl2nb3  48958  usgrexmpl2trifr  48961  pglem  49015  zlmodzxzldeplem3  49440  zlmodzxzldeplem4  49441  fv2prop  49638  rrx2pyel  49650  prelrrx2  49651  prelrrx2b  49652  rrx2pnecoorneor  49653  rrx2xpref1o  49656  rrx2plordisom  49661  ehl2eudisval0  49663  rrx2line  49678  rrx2linest  49680  rrx2linesl  49681  2sphere0  49688  line2ylem  49689  line2  49690  line2x  49692  line2y  49693  itscnhlinecirc02p  49723  inlinecirc02plem  49724