Theorem 2ex 11980

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  2c2 11958

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860  ax-addcl 10862

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-2 11966

This theorem is referenced by:  fzprval  13246  fztpval  13247  funcnvs3  14555  funcnvs4  14556  wrd3tpop  14589  wrdl3s3  14605  pmtrprfval  19010  m2detleiblem3  21686  m2detleiblem4  21687  ehl2eudis  24491  iblcnlem1  24857  gausslemma2dlem4  26422  2lgslem4  26459  addsqnreup  26496  selberglem1  26598  axlowdimlem4  27216  2wlkdlem4  28194  2pthdlem1  28196  umgrwwlks2on  28223  3wlkdlem4  28427  3wlkdlem5  28428  3pthdlem1  28429  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  eulerpathpr  28505  ex-ima  28707  s3rn  31122  cyc3evpm  31319  prodfzo03  32483  circlevma  32522  circlemethhgt  32523  hgt750lemg  32534  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgt  32543  rabren3dioph  40553  refsum2cnlem1  42469  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  zlmodzxzldeplem3  45731  zlmodzxzldeplem4  45732  fv2prop  45934  rrx2pyel  45946  prelrrx2  45947  prelrrx2b  45948  rrx2pnecoorneor  45949  rrx2xpref1o  45952  rrx2plordisom  45957  ehl2eudisval0  45959  rrx2line  45974  rrx2linest  45976  rrx2linesl  45977  2sphere0  45984  line2ylem  45985  line2  45986  line2x  45988  line2y  45989  itscnhlinecirc02p  46019  inlinecirc02plem  46020