MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  2ex Structured version   Visualization version   GIF version

Theorem 2ex 11706
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
StepHypRef Expression
1 2cn 11704 . 2 2 ∈ ℂ
21elexi 3512 1 2 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3493  cc 10527  2c2 11684
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-ext 2791  ax-1cn 10587  ax-addcl 10589
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-v 3495  df-2 11692
This theorem is referenced by:  fzprval  12960  fztpval  12961  funcnvs3  14268  funcnvs4  14269  wrd3tpop  14302  wrdl3s3  14318  pmtrprfval  18607  m2detleiblem3  21230  m2detleiblem4  21231  ehl2eudis  24017  iblcnlem1  24380  gausslemma2dlem4  25937  2lgslem4  25974  addsqnreup  26011  selberglem1  26113  axlowdimlem4  26723  2wlkdlem4  27699  2pthdlem1  27701  umgrwwlks2on  27728  3wlkdlem4  27933  3wlkdlem5  27934  3pthdlem1  27935  3wlkdlem10  27940  upgr3v3e3cycl  27951  upgr4cycl4dv4e  27956  eulerpathpr  28011  ex-ima  28213  s3rn  30615  cyc3evpm  30785  prodfzo03  31862  circlevma  31901  circlemethhgt  31902  hgt750lemg  31913  hgt750lemb  31915  hgt750lema  31916  hgt750leme  31917  tgoldbachgtde  31919  tgoldbachgt  31922  rabren3dioph  39397  refsum2cnlem1  41279  nnsum3primes4  43938  nnsum3primesgbe  43942  nnsum4primesodd  43946  nnsum4primesoddALTV  43947  zlmodzxzldeplem3  44542  zlmodzxzldeplem4  44543  fv2prop  44672  rrx2pyel  44684  prelrrx2  44685  prelrrx2b  44686  rrx2pnecoorneor  44687  rrx2xpref1o  44690  rrx2plordisom  44695  ehl2eudisval0  44697  rrx2line  44712  rrx2linest  44714  rrx2linesl  44715  2sphere0  44722  line2ylem  44723  line2  44724  line2x  44726  line2y  44727  itscnhlinecirc02p  44757  inlinecirc02plem  44758
  Copyright terms: Public domain W3C validator