Theorem 2ex 11304

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

Syntax hints:   ∈ wcel 2139  Vcvv 3340  ℂcc 10146  2c2 11282

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-resscn 10205  ax-1cn 10206  ax-icn 10207  ax-addcl 10208  ax-addrcl 10209  ax-mulcl 10210  ax-mulrcl 10211  ax-i2m1 10216  ax-1ne0 10217  ax-rrecex 10220  ax-cnre 10221

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6817  df-2 11291

This theorem is referenced by:  fzprval  12614  fztpval  12615  funcnvs3  13879  funcnvs4  13880  wrd3tpop  13912  wrdl3s3  13926  pmtrprfval  18127  m2detleiblem3  20657  m2detleiblem4  20658  iblcnlem1  23773  gausslemma2dlem4  25314  2lgslem4  25351  selberglem1  25454  axlowdimlem4  26045  2wlkdlem4  27069  2pthdlem1  27071  umgrwwlks2on  27099  3wlkdlem4  27335  3wlkdlem5  27336  3pthdlem1  27337  3wlkdlem10  27342  upgr3v3e3cycl  27353  upgr4cycl4dv4e  27358  eulerpathpr  27413  ex-ima  27631  prodfzo03  31011  circlevma  31050  circlemethhgt  31051  hgt750lemg  31062  hgt750lemb  31064  hgt750lema  31065  hgt750leme  31066  tgoldbachgtde  31068  tgoldbachgt  31071  rabren3dioph  37899  refsum2cnlem1  39713  nnsum3primes4  42204  nnsum3primesgbe  42208  nnsum4primesodd  42212  nnsum4primesoddALTV  42213  zlmodzxzldeplem3  42819  zlmodzxzldeplem4  42820