Theorem 2ex 12263

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066  2c2 12241

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11126  ax-addcl 11128

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-2 12249

This theorem is referenced by:  fzprval  13546  fztpval  13547  funcnvs3  14880  funcnvs4  14881  wrd3tpop  14914  wrdl3s3  14928  pmtrprfval  19417  m2detleiblem3  22516  m2detleiblem4  22517  ehl2eudis  25322  iblcnlem1  25689  gausslemma2dlem4  27280  2lgslem4  27317  addsqnreup  27354  selberglem1  27456  axlowdimlem4  28872  2wlkdlem4  29858  2pthdlem1  29860  umgrwwlks2on  29887  3wlkdlem4  30091  3wlkdlem5  30092  3pthdlem1  30093  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  eulerpathpr  30169  ex-ima  30371  s3rnOLD  32867  cyc3evpm  33107  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  rabren3dioph  42803  refsum2cnlem1  45031  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  cycl3grtrilem  47945  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2nb3  48025  usgrexmpl2trifr  48028  pglem  48082  zlmodzxzldeplem3  48491  zlmodzxzldeplem4  48492  fv2prop  48689  rrx2pyel  48701  prelrrx2  48702  prelrrx2b  48703  rrx2pnecoorneor  48704  rrx2xpref1o  48707  rrx2plordisom  48712  ehl2eudisval0  48714  rrx2line  48729  rrx2linest  48731  rrx2linesl  48732  2sphere0  48739  line2ylem  48740  line2  48741  line2x  48743  line2y  48744  itscnhlinecirc02p  48774  inlinecirc02plem  48775