Theorem 2ex 11702

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ℂcc 10524  2c2 11680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584  ax-addcl 10586

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-2 11688

This theorem is referenced by:  fzprval  12963  fztpval  12964  funcnvs3  14267  funcnvs4  14268  wrd3tpop  14301  wrdl3s3  14317  pmtrprfval  18607  m2detleiblem3  21234  m2detleiblem4  21235  ehl2eudis  24026  iblcnlem1  24391  gausslemma2dlem4  25953  2lgslem4  25990  addsqnreup  26027  selberglem1  26129  axlowdimlem4  26739  2wlkdlem4  27714  2pthdlem1  27716  umgrwwlks2on  27743  3wlkdlem4  27947  3wlkdlem5  27948  3pthdlem1  27949  3wlkdlem10  27954  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  eulerpathpr  28025  ex-ima  28227  s3rn  30648  cyc3evpm  30842  prodfzo03  31984  circlevma  32023  circlemethhgt  32024  hgt750lemg  32035  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  tgoldbachgt  32044  rabren3dioph  39756  refsum2cnlem1  41666  nnsum3primes4  44306  nnsum3primesgbe  44310  nnsum4primesodd  44314  nnsum4primesoddALTV  44315  zlmodzxzldeplem3  44911  zlmodzxzldeplem4  44912  fv2prop  45114  rrx2pyel  45126  prelrrx2  45127  prelrrx2b  45128  rrx2pnecoorneor  45129  rrx2xpref1o  45132  rrx2plordisom  45137  ehl2eudisval0  45139  rrx2line  45154  rrx2linest  45156  rrx2linesl  45157  2sphere0  45164  line2ylem  45165  line2  45166  line2x  45168  line2y  45169  itscnhlinecirc02p  45199  inlinecirc02plem  45200