Theorem 2ex 12270

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  2c2 12248

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 2702  ax-1cn 11133  ax-addcl 11135

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-2 12256

This theorem is referenced by:  fzprval  13553  fztpval  13554  funcnvs3  14887  funcnvs4  14888  wrd3tpop  14921  wrdl3s3  14935  pmtrprfval  19424  m2detleiblem3  22523  m2detleiblem4  22524  ehl2eudis  25329  iblcnlem1  25696  gausslemma2dlem4  27287  2lgslem4  27324  addsqnreup  27361  selberglem1  27463  axlowdimlem4  28879  2wlkdlem4  29865  2pthdlem1  29867  umgrwwlks2on  29894  3wlkdlem4  30098  3wlkdlem5  30099  3pthdlem1  30100  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  eulerpathpr  30176  ex-ima  30378  s3rnOLD  32874  cyc3evpm  33114  prodfzo03  34601  circlevma  34640  circlemethhgt  34641  hgt750lemg  34652  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgt  34661  rabren3dioph  42810  refsum2cnlem1  45038  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  cycl3grtrilem  47949  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2nb3  48029  usgrexmpl2trifr  48032  pglem  48086  zlmodzxzldeplem3  48495  zlmodzxzldeplem4  48496  fv2prop  48693  rrx2pyel  48705  prelrrx2  48706  prelrrx2b  48707  rrx2pnecoorneor  48708  rrx2xpref1o  48711  rrx2plordisom  48716  ehl2eudisval0  48718  rrx2line  48733  rrx2linest  48735  rrx2linesl  48736  2sphere0  48743  line2ylem  48744  line2  48745  line2x  48747  line2y  48748  itscnhlinecirc02p  48778  inlinecirc02plem  48779