Theorem 2ex 11173

Description: 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 11172	. 2 ⊢ 2 ∈ ℂ
2	1	elexi 3285	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 2071  Vcvv 3272  ℂcc 10015  2c2 11151

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1818  ax-5 1920  ax-6 1986  ax-7 2022  ax-9 2080  ax-10 2100  ax-11 2115  ax-12 2128  ax-13 2323  ax-ext 2672  ax-resscn 10074  ax-1cn 10075  ax-icn 10076  ax-addcl 10077  ax-addrcl 10078  ax-mulcl 10079  ax-mulrcl 10080  ax-i2m1 10085  ax-1ne0 10086  ax-rrecex 10089  ax-cnre 10090

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1567  df-ex 1786  df-nf 1791  df-sb 1979  df-clab 2679  df-cleq 2685  df-clel 2688  df-nfc 2823  df-ne 2865  df-ral 2987  df-rex 2988  df-rab 2991  df-v 3274  df-dif 3651  df-un 3653  df-in 3655  df-ss 3662  df-nul 3992  df-if 4163  df-sn 4254  df-pr 4256  df-op 4260  df-uni 4513  df-br 4729  df-iota 5932  df-fv 5977  df-ov 6736  df-2 11160

This theorem is referenced by:  fzprval  12483  fztpval  12484  funcnvs3  13748  funcnvs4  13749  wrd3tpop  13781  wrdl3s3  13795  pmtrprfval  17996  m2detleiblem3  20526  m2detleiblem4  20527  iblcnlem1  23642  gausslemma2dlem4  25182  2lgslem4  25219  selberglem1  25322  axlowdimlem4  25913  2wlkdlem4  26937  2pthdlem1  26939  umgrwwlks2on  26967  3wlkdlem4  27203  3wlkdlem5  27204  3pthdlem1  27205  3wlkdlem10  27210  upgr3v3e3cycl  27221  upgr4cycl4dv4e  27226  eulerpathpr  27281  ex-ima  27499  prodfzo03  30879  circlevma  30918  circlemethhgt  30919  hgt750lemg  30930  hgt750lemb  30932  hgt750lema  30933  hgt750leme  30934  tgoldbachgtde  30936  tgoldbachgt  30939  rabren3dioph  37766  refsum2cnlem1  39580  nnsum3primes4  42071  nnsum3primesgbe  42075  nnsum4primesodd  42079  nnsum4primesoddALTV  42080  zlmodzxzldeplem3  42686  zlmodzxzldeplem4  42687