Theorem 2ex 12289

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ℂcc 11108  2c2 12267

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168  ax-addcl 11170

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-2 12275

This theorem is referenced by:  fzprval  13562  fztpval  13563  funcnvs3  14865  funcnvs4  14866  wrd3tpop  14899  wrdl3s3  14913  pmtrprfval  19355  m2detleiblem3  22131  m2detleiblem4  22132  ehl2eudis  24939  iblcnlem1  25305  gausslemma2dlem4  26872  2lgslem4  26909  addsqnreup  26946  selberglem1  27048  axlowdimlem4  28203  2wlkdlem4  29182  2pthdlem1  29184  umgrwwlks2on  29211  3wlkdlem4  29415  3wlkdlem5  29416  3pthdlem1  29417  3wlkdlem10  29422  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  eulerpathpr  29493  ex-ima  29695  s3rn  32112  cyc3evpm  32309  prodfzo03  33615  circlevma  33654  circlemethhgt  33655  hgt750lemg  33666  hgt750lemb  33668  hgt750lema  33669  hgt750leme  33670  tgoldbachgtde  33672  tgoldbachgt  33675  rabren3dioph  41553  refsum2cnlem1  43721  nnsum3primes4  46456  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  zlmodzxzldeplem3  47183  zlmodzxzldeplem4  47184  fv2prop  47386  rrx2pyel  47398  prelrrx2  47399  prelrrx2b  47400  rrx2pnecoorneor  47401  rrx2xpref1o  47404  rrx2plordisom  47409  ehl2eudisval0  47411  rrx2line  47426  rrx2linest  47428  rrx2linesl  47429  2sphere0  47436  line2ylem  47437  line2  47438  line2x  47440  line2y  47441  itscnhlinecirc02p  47471  inlinecirc02plem  47472