Theorem 2ex 12309

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

Syntax hints:   ∈ wcel 2145  Vcvv 3457  ℂcc 11086  2c2 12286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-1cn 11146  ax-addcl 11148

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-2 12294

This theorem is referenced by:  fzprval  13604  fztpval  13605  funcnvs3  14941  funcnvs4  14942  wrd3tpop  14975  wrdl3s3  14989  ex-chn1  18683  pmtrprfval  19548  m2detleiblem3  22747  m2detleiblem4  22748  ehl2eudis  25542  iblcnlem1  25908  gausslemma2dlem4  27491  2lgslem4  27528  addsqnreup  27565  selberglem1  27667  axlowdimlem4  29204  2wlkdlem4  30186  2pthdlem1  30188  usgrwwlks2on  30216  umgrwwlks2on  30217  3wlkdlem4  30422  3wlkdlem5  30423  3pthdlem1  30424  3wlkdlem10  30429  upgr3v3e3cycl  30440  upgr4cycl4dv4e  30445  eulerpathpr  30500  ex-ima  30702  s3rnOLD  33179  cyc3evpm  33383  prodfzo03  34907  circlevma  34946  circlemethhgt  34947  hgt750lemg  34958  hgt750lemb  34960  hgt750lema  34961  hgt750leme  34962  tgoldbachgtde  34964  tgoldbachgt  34967  rabren3dioph  43404  refsum2cnlem1  45615  nthrucw  47460  nnsum3primes4  48408  nnsum3primesgbe  48412  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  cycl3grtrilem  48566  usgrexmpl1lem  48641  usgrexmpl1tri  48645  usgrexmpl2lem  48646  usgrexmpl2nb0  48651  usgrexmpl2nb1  48652  usgrexmpl2nb2  48653  usgrexmpl2nb3  48654  usgrexmpl2trifr  48657  pglem  48711  zlmodzxzldeplem3  49133  zlmodzxzldeplem4  49134  fv2prop  49331  rrx2pyel  49343  prelrrx2  49344  prelrrx2b  49345  rrx2pnecoorneor  49346  rrx2xpref1o  49349  rrx2plordisom  49354  ehl2eudisval0  49356  rrx2line  49371  rrx2linest  49373  rrx2linesl  49374  2sphere0  49381  line2ylem  49382  line2  49383  line2x  49385  line2y  49386  itscnhlinecirc02p  49416  inlinecirc02plem  49417