Theorem 2ex 11713

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

Syntax hints:   ∈ wcel 2110  Vcvv 3494  ℂcc 10534  2c2 11691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-ext 2793  ax-1cn 10594  ax-addcl 10596

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-v 3496  df-2 11699

This theorem is referenced by:  fzprval  12967  fztpval  12968  funcnvs3  14275  funcnvs4  14276  wrd3tpop  14309  wrdl3s3  14325  pmtrprfval  18614  m2detleiblem3  21237  m2detleiblem4  21238  ehl2eudis  24024  iblcnlem1  24387  gausslemma2dlem4  25944  2lgslem4  25981  addsqnreup  26018  selberglem1  26120  axlowdimlem4  26730  2wlkdlem4  27706  2pthdlem1  27708  umgrwwlks2on  27735  3wlkdlem4  27940  3wlkdlem5  27941  3pthdlem1  27942  3wlkdlem10  27947  upgr3v3e3cycl  27958  upgr4cycl4dv4e  27963  eulerpathpr  28018  ex-ima  28220  s3rn  30622  cyc3evpm  30792  prodfzo03  31874  circlevma  31913  circlemethhgt  31914  hgt750lemg  31925  hgt750lemb  31927  hgt750lema  31928  hgt750leme  31929  tgoldbachgtde  31931  tgoldbachgt  31934  rabren3dioph  39410  refsum2cnlem1  41292  nnsum3primes4  43952  nnsum3primesgbe  43956  nnsum4primesodd  43960  nnsum4primesoddALTV  43961  zlmodzxzldeplem3  44556  zlmodzxzldeplem4  44557  fv2prop  44686  rrx2pyel  44698  prelrrx2  44699  prelrrx2b  44700  rrx2pnecoorneor  44701  rrx2xpref1o  44704  rrx2plordisom  44709  ehl2eudisval0  44711  rrx2line  44726  rrx2linest  44728  rrx2linesl  44729  2sphere0  44736  line2ylem  44737  line2  44738  line2x  44740  line2y  44741  itscnhlinecirc02p  44771  inlinecirc02plem  44772