Theorem 2ex 11037

Description: 2 is a set (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
2ex	⊢ 2 ∈ V

Proof of Theorem 2ex

Step	Hyp	Ref	Expression
1		2cn 11036	. 2 ⊢ 2 ∈ ℂ
2	1	elexi 3204	1 ⊢ 2 ∈ V

Syntax hints:   ∈ wcel 1992  Vcvv 3191  ℂcc 9879  2c2 11015

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-i2m1 9949  ax-1ne0 9950  ax-rrecex 9953  ax-cnre 9954

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3193  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-br 4619  df-iota 5813  df-fv 5858  df-ov 6608  df-2 11024

This theorem is referenced by:  fzprval  12340  fztpval  12341  funcnvs3  13590  funcnvs4  13591  wrd3tpop  13620  wrdl3s3  13634  pmtrprfval  17823  m2detleiblem3  20349  m2detleiblem4  20350  iblcnlem1  23455  gausslemma2dlem4  24989  2lgslem4  25026  selberglem1  25129  axlowdimlem4  25720  2wlkdlem4  26687  2pthdlem1  26689  umgrwwlks2on  26713  3wlkdlem4  26882  3wlkdlem5  26883  3pthdlem1  26884  3wlkdlem10  26889  upgr3v3e3cycl  26900  upgr4cycl4dv4e  26905  eulerpathpr  26960  ex-ima  27147  rabren3dioph  36845  refsum2cnlem1  38665  nnsum3primes4  40953  nnsum3primesgbe  40957  nnsum4primesodd  40961  nnsum4primesoddALTV  40962  zlmodzxzldeplem3  41553  zlmodzxzldeplem4  41554