Theorem 2ex 12223

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ℂcc 11026  2c2 12201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086  ax-addcl 11088

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-2 12209

This theorem is referenced by:  fzprval  13506  fztpval  13507  funcnvs3  14839  funcnvs4  14840  wrd3tpop  14873  wrdl3s3  14887  pmtrprfval  19384  m2detleiblem3  22532  m2detleiblem4  22533  ehl2eudis  25338  iblcnlem1  25705  gausslemma2dlem4  27296  2lgslem4  27333  addsqnreup  27370  selberglem1  27472  axlowdimlem4  28908  2wlkdlem4  29891  2pthdlem1  29893  umgrwwlks2on  29920  3wlkdlem4  30124  3wlkdlem5  30125  3pthdlem1  30126  3wlkdlem10  30131  upgr3v3e3cycl  30142  upgr4cycl4dv4e  30147  eulerpathpr  30202  ex-ima  30404  s3rnOLD  32900  cyc3evpm  33105  prodfzo03  34570  circlevma  34609  circlemethhgt  34610  hgt750lemg  34621  hgt750lemb  34623  hgt750lema  34624  hgt750leme  34625  tgoldbachgtde  34627  tgoldbachgt  34630  rabren3dioph  42788  refsum2cnlem1  45015  nnsum3primes4  47773  nnsum3primesgbe  47777  nnsum4primesodd  47781  nnsum4primesoddALTV  47782  cycl3grtrilem  47931  usgrexmpl1lem  48006  usgrexmpl1tri  48010  usgrexmpl2lem  48011  usgrexmpl2nb0  48016  usgrexmpl2nb1  48017  usgrexmpl2nb2  48018  usgrexmpl2nb3  48019  usgrexmpl2trifr  48022  pglem  48076  zlmodzxzldeplem3  48488  zlmodzxzldeplem4  48489  fv2prop  48686  rrx2pyel  48698  prelrrx2  48699  prelrrx2b  48700  rrx2pnecoorneor  48701  rrx2xpref1o  48704  rrx2plordisom  48709  ehl2eudisval0  48711  rrx2line  48726  rrx2linest  48728  rrx2linesl  48729  2sphere0  48736  line2ylem  48737  line2  48738  line2x  48740  line2y  48741  itscnhlinecirc02p  48771  inlinecirc02plem  48772