Theorem 2ex 12450

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11228  2c2 12427

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11288  ax-addcl 11290

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-2 12435

This theorem is used by:  fzprval  13749  fztpval  13750  funcnvs3  15097  funcnvs4  15098  wrd3tpop  15131  s3rex  15133  wrdl3s3  15147  ex-chn1  18843  pmtrprfval  19734  m2detleiblem3  22977  m2detleiblem4  22978  iblcnlem1  26141  gausslemma2dlem4  27729  2lgslem4  27766  addsqnreup  27803  selberglem1  27905  elcgrabasi  29408  axlowdimlem4  29556  2wlkdlem4  30550  2pthdlem1  30552  usgrwwlks2on  30580  umgrwwlks2on  30581  3wlkdlem4  30796  3wlkdlem5  30797  3pthdlem1  30798  3wlkdlem10  30803  upgr3v3e3cycl  30814  upgr4cycl4dv4e  30819  eulerpathpr  30874  ex-ima  31076  cyc3evpm  33787  prodfzo03  35315  circlevma  35354  circlemethhgt  35355  hgt750lemg  35366  hgt750lemb  35368  hgt750lema  35369  hgt750leme  35370  tgoldbachgtde  35372  tgoldbachgt  35375  rabren3dioph  44026  refsum2cnlem1  46270  nnsum3primes4  49101  nnsum3primesgbe  49105  nnsum4primesodd  49109  nnsum4primesoddALTV  49110  cycl3grtrilem  49259  usgrexmpl1lem  49334  usgrexmpl1tri  49338  usgrexmpl2lem  49339  usgrexmpl2nb0  49344  usgrexmpl2nb1  49345  usgrexmpl2nb2  49346  usgrexmpl2nb3  49347  usgrexmpl2trifr  49350  pglem  49404  zlmodzxzldeplem3  49829  zlmodzxzldeplem4  49830  fv2prop  50027  line2  50079