Theorem 2ex 12340

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ℂcc 11150  2c2 12318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-1cn 11210  ax-addcl 11212

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-2 12326

This theorem is referenced by:  fzprval  13621  fztpval  13622  funcnvs3  14949  funcnvs4  14950  wrd3tpop  14983  wrdl3s3  14997  pmtrprfval  19519  m2detleiblem3  22650  m2detleiblem4  22651  ehl2eudis  25469  iblcnlem1  25837  gausslemma2dlem4  27427  2lgslem4  27464  addsqnreup  27501  selberglem1  27603  axlowdimlem4  28974  2wlkdlem4  29957  2pthdlem1  29959  umgrwwlks2on  29986  3wlkdlem4  30190  3wlkdlem5  30191  3pthdlem1  30192  3wlkdlem10  30197  upgr3v3e3cycl  30208  upgr4cycl4dv4e  30213  eulerpathpr  30268  ex-ima  30470  s3rnOLD  32914  cyc3evpm  33152  prodfzo03  34596  circlevma  34635  circlemethhgt  34636  hgt750lemg  34647  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  rabren3dioph  42802  refsum2cnlem1  44974  nnsum3primes4  47712  nnsum3primesgbe  47716  nnsum4primesodd  47720  nnsum4primesoddALTV  47721  usgrexmpl1lem  47915  usgrexmpl1tri  47919  usgrexmpl2lem  47920  usgrexmpl2nb0  47925  usgrexmpl2nb1  47926  usgrexmpl2nb2  47927  usgrexmpl2nb3  47928  usgrexmpl2trifr  47931  zlmodzxzldeplem3  48347  zlmodzxzldeplem4  48348  fv2prop  48549  rrx2pyel  48561  prelrrx2  48562  prelrrx2b  48563  rrx2pnecoorneor  48564  rrx2xpref1o  48567  rrx2plordisom  48572  ehl2eudisval0  48574  rrx2line  48589  rrx2linest  48591  rrx2linesl  48592  2sphere0  48599  line2ylem  48600  line2  48601  line2x  48603  line2y  48604  itscnhlinecirc02p  48634  inlinecirc02plem  48635