Theorem 2ex 12320

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

Syntax hints:   ∈ wcel 2099  Vcvv 3471  ℂcc 11137  2c2 12298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11197  ax-addcl 11199

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-2 12306

This theorem is referenced by:  fzprval  13595  fztpval  13596  funcnvs3  14898  funcnvs4  14899  wrd3tpop  14932  wrdl3s3  14946  pmtrprfval  19442  m2detleiblem3  22544  m2detleiblem4  22545  ehl2eudis  25363  iblcnlem1  25730  gausslemma2dlem4  27315  2lgslem4  27352  addsqnreup  27389  selberglem1  27491  axlowdimlem4  28769  2wlkdlem4  29752  2pthdlem1  29754  umgrwwlks2on  29781  3wlkdlem4  29985  3wlkdlem5  29986  3pthdlem1  29987  3wlkdlem10  29992  upgr3v3e3cycl  30003  upgr4cycl4dv4e  30008  eulerpathpr  30063  ex-ima  30265  s3rn  32682  cyc3evpm  32884  prodfzo03  34235  circlevma  34274  circlemethhgt  34275  hgt750lemg  34286  hgt750lemb  34288  hgt750lema  34289  hgt750leme  34290  tgoldbachgtde  34292  tgoldbachgt  34295  rabren3dioph  42235  refsum2cnlem1  44399  nnsum3primes4  47128  nnsum3primesgbe  47132  nnsum4primesodd  47136  nnsum4primesoddALTV  47137  zlmodzxzldeplem3  47570  zlmodzxzldeplem4  47571  fv2prop  47773  rrx2pyel  47785  prelrrx2  47786  prelrrx2b  47787  rrx2pnecoorneor  47788  rrx2xpref1o  47791  rrx2plordisom  47796  ehl2eudisval0  47798  rrx2line  47813  rrx2linest  47815  rrx2linesl  47816  2sphere0  47823  line2ylem  47824  line2  47825  line2x  47827  line2y  47828  itscnhlinecirc02p  47858  inlinecirc02plem  47859