Theorem 2ex 12343

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153  2c2 12321

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213  ax-addcl 11215

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-2 12329

This theorem is referenced by:  fzprval  13625  fztpval  13626  funcnvs3  14953  funcnvs4  14954  wrd3tpop  14987  wrdl3s3  15001  pmtrprfval  19505  m2detleiblem3  22635  m2detleiblem4  22636  ehl2eudis  25456  iblcnlem1  25823  gausslemma2dlem4  27413  2lgslem4  27450  addsqnreup  27487  selberglem1  27589  axlowdimlem4  28960  2wlkdlem4  29948  2pthdlem1  29950  umgrwwlks2on  29977  3wlkdlem4  30181  3wlkdlem5  30182  3pthdlem1  30183  3wlkdlem10  30188  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  eulerpathpr  30259  ex-ima  30461  s3rnOLD  32930  cyc3evpm  33170  prodfzo03  34618  circlevma  34657  circlemethhgt  34658  hgt750lemg  34669  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  rabren3dioph  42826  refsum2cnlem1  45042  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  cycl3grtrilem  47913  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2nb3  47993  usgrexmpl2trifr  47996  zlmodzxzldeplem3  48419  zlmodzxzldeplem4  48420  fv2prop  48621  rrx2pyel  48633  prelrrx2  48634  prelrrx2b  48635  rrx2pnecoorneor  48636  rrx2xpref1o  48639  rrx2plordisom  48644  ehl2eudisval0  48646  rrx2line  48661  rrx2linest  48663  rrx2linesl  48664  2sphere0  48671  line2ylem  48672  line2  48673  line2x  48675  line2y  48676  itscnhlinecirc02p  48706  inlinecirc02plem  48707