Theorem 2ex 12311

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

Syntax hints:   ∈ wcel 2099  Vcvv 3469  ℂcc 11128  2c2 12289

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 2698  ax-1cn 11188  ax-addcl 11190

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-2 12297

This theorem is referenced by:  fzprval  13586  fztpval  13587  funcnvs3  14889  funcnvs4  14890  wrd3tpop  14923  wrdl3s3  14937  pmtrprfval  19433  m2detleiblem3  22518  m2detleiblem4  22519  ehl2eudis  25337  iblcnlem1  25704  gausslemma2dlem4  27289  2lgslem4  27326  addsqnreup  27363  selberglem1  27465  axlowdimlem4  28743  2wlkdlem4  29726  2pthdlem1  29728  umgrwwlks2on  29755  3wlkdlem4  29959  3wlkdlem5  29960  3pthdlem1  29961  3wlkdlem10  29966  upgr3v3e3cycl  29977  upgr4cycl4dv4e  29982  eulerpathpr  30037  ex-ima  30239  s3rn  32651  cyc3evpm  32849  prodfzo03  34171  circlevma  34210  circlemethhgt  34211  hgt750lemg  34222  hgt750lemb  34224  hgt750lema  34225  hgt750leme  34226  tgoldbachgtde  34228  tgoldbachgt  34231  rabren3dioph  42157  refsum2cnlem1  44322  nnsum3primes4  47051  nnsum3primesgbe  47055  nnsum4primesodd  47059  nnsum4primesoddALTV  47060  zlmodzxzldeplem3  47493  zlmodzxzldeplem4  47494  fv2prop  47696  rrx2pyel  47708  prelrrx2  47709  prelrrx2b  47710  rrx2pnecoorneor  47711  rrx2xpref1o  47714  rrx2plordisom  47719  ehl2eudisval0  47721  rrx2line  47736  rrx2linest  47738  rrx2linesl  47739  2sphere0  47746  line2ylem  47747  line2  47748  line2x  47750  line2y  47751  itscnhlinecirc02p  47781  inlinecirc02plem  47782