Theorem 2ex 11717

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ℂcc 10537  2c2 11695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597  ax-addcl 10599

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498  df-2 11703

This theorem is referenced by:  fzprval  12971  fztpval  12972  funcnvs3  14278  funcnvs4  14279  wrd3tpop  14312  wrdl3s3  14328  pmtrprfval  18617  m2detleiblem3  21240  m2detleiblem4  21241  ehl2eudis  24027  iblcnlem1  24390  gausslemma2dlem4  25947  2lgslem4  25984  addsqnreup  26021  selberglem1  26123  axlowdimlem4  26733  2wlkdlem4  27709  2pthdlem1  27711  umgrwwlks2on  27738  3wlkdlem4  27943  3wlkdlem5  27944  3pthdlem1  27945  3wlkdlem10  27950  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  eulerpathpr  28021  ex-ima  28223  s3rn  30624  cyc3evpm  30794  prodfzo03  31876  circlevma  31915  circlemethhgt  31916  hgt750lemg  31927  hgt750lemb  31929  hgt750lema  31930  hgt750leme  31931  tgoldbachgtde  31933  tgoldbachgt  31936  rabren3dioph  39419  refsum2cnlem1  41301  nnsum3primes4  43960  nnsum3primesgbe  43964  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  zlmodzxzldeplem3  44564  zlmodzxzldeplem4  44565  fv2prop  44694  rrx2pyel  44706  prelrrx2  44707  prelrrx2b  44708  rrx2pnecoorneor  44709  rrx2xpref1o  44712  rrx2plordisom  44717  ehl2eudisval0  44719  rrx2line  44734  rrx2linest  44736  rrx2linesl  44737  2sphere0  44744  line2ylem  44745  line2  44746  line2x  44748  line2y  44749  itscnhlinecirc02p  44779  inlinecirc02plem  44780