Theorem 2ex 12222

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  2c2 12200

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084  ax-addcl 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-2 12208

This theorem is referenced by:  fzprval  13501  fztpval  13502  funcnvs3  14837  funcnvs4  14838  wrd3tpop  14871  wrdl3s3  14885  ex-chn1  18560  pmtrprfval  19416  m2detleiblem3  22573  m2detleiblem4  22574  ehl2eudis  25378  iblcnlem1  25745  gausslemma2dlem4  27336  2lgslem4  27373  addsqnreup  27410  selberglem1  27512  axlowdimlem4  29018  2wlkdlem4  30001  2pthdlem1  30003  usgrwwlks2on  30031  umgrwwlks2on  30032  3wlkdlem4  30237  3wlkdlem5  30238  3pthdlem1  30239  3wlkdlem10  30244  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  eulerpathpr  30315  ex-ima  30517  s3rnOLD  33028  cyc3evpm  33232  prodfzo03  34760  circlevma  34799  circlemethhgt  34800  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgt  34820  rabren3dioph  43053  refsum2cnlem1  45278  nthrucw  47126  nnsum3primes4  48030  nnsum3primesgbe  48034  nnsum4primesodd  48038  nnsum4primesoddALTV  48039  cycl3grtrilem  48188  usgrexmpl1lem  48263  usgrexmpl1tri  48267  usgrexmpl2lem  48268  usgrexmpl2nb0  48273  usgrexmpl2nb1  48274  usgrexmpl2nb2  48275  usgrexmpl2nb3  48276  usgrexmpl2trifr  48279  pglem  48333  zlmodzxzldeplem3  48744  zlmodzxzldeplem4  48745  fv2prop  48942  rrx2pyel  48954  prelrrx2  48955  prelrrx2b  48956  rrx2pnecoorneor  48957  rrx2xpref1o  48960  rrx2plordisom  48965  ehl2eudisval0  48967  rrx2line  48982  rrx2linest  48984  rrx2linesl  48985  2sphere0  48992  line2ylem  48993  line2  48994  line2x  48996  line2y  48997  itscnhlinecirc02p  49027  inlinecirc02plem  49028