Theorem 2ex 12256

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  ℂcc 11034  2c2 12234

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-1cn 11094  ax-addcl 11096

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-2 12242

This theorem is referenced by:  fzprval  13537  fztpval  13538  funcnvs3  14874  funcnvs4  14875  wrd3tpop  14908  wrdl3s3  14922  ex-chn1  18601  pmtrprfval  19460  m2detleiblem3  22619  m2detleiblem4  22620  ehl2eudis  25414  iblcnlem1  25780  gausslemma2dlem4  27357  2lgslem4  27394  addsqnreup  27431  selberglem1  27533  axlowdimlem4  29039  2wlkdlem4  30021  2pthdlem1  30023  usgrwwlks2on  30051  umgrwwlks2on  30052  3wlkdlem4  30257  3wlkdlem5  30258  3pthdlem1  30259  3wlkdlem10  30264  upgr3v3e3cycl  30275  upgr4cycl4dv4e  30280  eulerpathpr  30335  ex-ima  30537  s3rnOLD  33032  cyc3evpm  33238  prodfzo03  34794  circlevma  34833  circlemethhgt  34834  hgt750lemg  34845  hgt750lemb  34847  hgt750lema  34848  hgt750leme  34849  tgoldbachgtde  34851  tgoldbachgt  34854  rabren3dioph  43267  refsum2cnlem1  45492  nthrucw  47338  nnsum3primes4  48286  nnsum3primesgbe  48290  nnsum4primesodd  48294  nnsum4primesoddALTV  48295  cycl3grtrilem  48444  usgrexmpl1lem  48519  usgrexmpl1tri  48523  usgrexmpl2lem  48524  usgrexmpl2nb0  48529  usgrexmpl2nb1  48530  usgrexmpl2nb2  48531  usgrexmpl2nb3  48532  usgrexmpl2trifr  48535  pglem  48589  zlmodzxzldeplem3  49000  zlmodzxzldeplem4  49001  fv2prop  49198  rrx2pyel  49210  prelrrx2  49211  prelrrx2b  49212  rrx2pnecoorneor  49213  rrx2xpref1o  49216  rrx2plordisom  49221  ehl2eudisval0  49223  rrx2line  49238  rrx2linest  49240  rrx2linesl  49241  2sphere0  49248  line2ylem  49249  line2  49250  line2x  49252  line2y  49253  itscnhlinecirc02p  49283  inlinecirc02plem  49284