Theorem 2ex 12370

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ℂcc 11182  2c2 12348

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242  ax-addcl 11244

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-2 12356

This theorem is referenced by:  fzprval  13645  fztpval  13646  funcnvs3  14963  funcnvs4  14964  wrd3tpop  14997  wrdl3s3  15011  pmtrprfval  19529  m2detleiblem3  22656  m2detleiblem4  22657  ehl2eudis  25475  iblcnlem1  25843  gausslemma2dlem4  27431  2lgslem4  27468  addsqnreup  27505  selberglem1  27607  axlowdimlem4  28978  2wlkdlem4  29961  2pthdlem1  29963  umgrwwlks2on  29990  3wlkdlem4  30194  3wlkdlem5  30195  3pthdlem1  30196  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  eulerpathpr  30272  ex-ima  30474  s3rnOLD  32912  cyc3evpm  33143  prodfzo03  34580  circlevma  34619  circlemethhgt  34620  hgt750lemg  34631  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgt  34640  rabren3dioph  42771  refsum2cnlem1  44937  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2nb3  47849  usgrexmpl2trifr  47852  zlmodzxzldeplem3  48231  zlmodzxzldeplem4  48232  fv2prop  48434  rrx2pyel  48446  prelrrx2  48447  prelrrx2b  48448  rrx2pnecoorneor  48449  rrx2xpref1o  48452  rrx2plordisom  48457  ehl2eudisval0  48459  rrx2line  48474  rrx2linest  48476  rrx2linesl  48477  2sphere0  48484  line2ylem  48485  line2  48486  line2x  48488  line2y  48489  itscnhlinecirc02p  48519  inlinecirc02plem  48520