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

Theorem 2ex 12235
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 12233 . 2 2 ∈ ℂ
21elexi 3463 1 2 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3444  cc 11054  2c2 12213
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11114  ax-addcl 11116
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-2 12221
This theorem is referenced by:  fzprval  13508  fztpval  13509  funcnvs3  14809  funcnvs4  14810  wrd3tpop  14843  wrdl3s3  14857  pmtrprfval  19274  m2detleiblem3  21994  m2detleiblem4  21995  ehl2eudis  24802  iblcnlem1  25168  gausslemma2dlem4  26733  2lgslem4  26770  addsqnreup  26807  selberglem1  26909  axlowdimlem4  27936  2wlkdlem4  28915  2pthdlem1  28917  umgrwwlks2on  28944  3wlkdlem4  29148  3wlkdlem5  29149  3pthdlem1  29150  3wlkdlem10  29155  upgr3v3e3cycl  29166  upgr4cycl4dv4e  29171  eulerpathpr  29226  ex-ima  29428  s3rn  31851  cyc3evpm  32048  prodfzo03  33273  circlevma  33312  circlemethhgt  33313  hgt750lemg  33324  hgt750lemb  33326  hgt750lema  33327  hgt750leme  33328  tgoldbachgtde  33330  tgoldbachgt  33333  rabren3dioph  41181  refsum2cnlem1  43330  nnsum3primes4  46066  nnsum3primesgbe  46070  nnsum4primesodd  46074  nnsum4primesoddALTV  46075  zlmodzxzldeplem3  46669  zlmodzxzldeplem4  46670  fv2prop  46872  rrx2pyel  46884  prelrrx2  46885  prelrrx2b  46886  rrx2pnecoorneor  46887  rrx2xpref1o  46890  rrx2plordisom  46895  ehl2eudisval0  46897  rrx2line  46912  rrx2linest  46914  rrx2linesl  46915  2sphere0  46922  line2ylem  46923  line2  46924  line2x  46926  line2y  46927  itscnhlinecirc02p  46957  inlinecirc02plem  46958
  Copyright terms: Public domain W3C validator