Theorem 2ex 12336

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  ℂcc 11116  2c2 12313

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-1cn 11176  ax-addcl 11178

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-2 12321

This theorem is used by:  fzprval  13632  fztpval  13633  funcnvs3  14977  funcnvs4  14978  wrd3tpop  15011  wrdl3s3  15025  ex-chn1  18718  pmtrprfval  19588  m2detleiblem3  22823  m2detleiblem4  22824  ehl2eudis  25618  iblcnlem1  25984  gausslemma2dlem4  27570  2lgslem4  27607  addsqnreup  27644  selberglem1  27746  axlowdimlem4  29332  2wlkdlem4  30314  2pthdlem1  30316  usgrwwlks2on  30344  umgrwwlks2on  30345  3wlkdlem4  30550  3wlkdlem5  30551  3pthdlem1  30552  3wlkdlem10  30557  upgr3v3e3cycl  30568  upgr4cycl4dv4e  30573  eulerpathpr  30628  ex-ima  30830  cyc3evpm  33501  prodfzo03  35022  circlevma  35061  circlemethhgt  35062  hgt750lemg  35073  hgt750lemb  35075  hgt750lema  35076  hgt750leme  35077  tgoldbachgtde  35079  tgoldbachgt  35082  rabren3dioph  43583  refsum2cnlem1  45798  nnsum3primes4  48594  nnsum3primesgbe  48598  nnsum4primesodd  48602  nnsum4primesoddALTV  48603  cycl3grtrilem  48752  usgrexmpl1lem  48827  usgrexmpl1tri  48831  usgrexmpl2lem  48832  usgrexmpl2nb0  48837  usgrexmpl2nb1  48838  usgrexmpl2nb2  48839  usgrexmpl2nb3  48840  usgrexmpl2trifr  48843  pglem  48897  zlmodzxzldeplem3  49323  zlmodzxzldeplem4  49324  fv2prop  49521  rrx2pyel  49533  prelrrx2  49534  prelrrx2b  49535  rrx2pnecoorneor  49536  rrx2xpref1o  49539  rrx2plordisom  49544  ehl2eudisval0  49546  rrx2line  49561  rrx2linest  49563  rrx2linesl  49564  2sphere0  49571  line2ylem  49572  line2  49573  line2x  49575  line2y  49576  itscnhlinecirc02p  49606  inlinecirc02plem  49607