Theorem 2ex 12423

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ℂcc 11201  2c2 12400

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-1cn 11261  ax-addcl 11263

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-2 12408

This theorem is used by:  fzprval  13722  fztpval  13723  funcnvs3  15070  funcnvs4  15071  wrd3tpop  15104  s3rex  15106  wrdl3s3  15120  ex-chn1  18816  pmtrprfval  19706  m2detleiblem3  22949  m2detleiblem4  22950  iblcnlem1  26113  gausslemma2dlem4  27701  2lgslem4  27738  addsqnreup  27775  selberglem1  27877  elcgrabasi  29380  axlowdimlem4  29528  2wlkdlem4  30522  2pthdlem1  30524  usgrwwlks2on  30552  umgrwwlks2on  30553  3wlkdlem4  30768  3wlkdlem5  30769  3pthdlem1  30770  3wlkdlem10  30775  upgr3v3e3cycl  30786  upgr4cycl4dv4e  30791  eulerpathpr  30846  ex-ima  31048  cyc3evpm  33757  prodfzo03  35278  circlevma  35317  circlemethhgt  35318  hgt750lemg  35329  hgt750lemb  35331  hgt750lema  35332  hgt750leme  35333  tgoldbachgtde  35335  tgoldbachgt  35338  rabren3dioph  43915  refsum2cnlem1  46147  nnsum3primes4  48979  nnsum3primesgbe  48983  nnsum4primesodd  48987  nnsum4primesoddALTV  48988  cycl3grtrilem  49137  usgrexmpl1lem  49212  usgrexmpl1tri  49216  usgrexmpl2lem  49217  usgrexmpl2nb0  49222  usgrexmpl2nb1  49223  usgrexmpl2nb2  49224  usgrexmpl2nb3  49225  usgrexmpl2trifr  49228  pglem  49282  zlmodzxzldeplem3  49707  zlmodzxzldeplem4  49708  fv2prop  49905  line2  49957