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

Theorem 2ex 11429
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 11427 . 2 2 ∈ ℂ
21elexi 3431 1 2 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2166  Vcvv 3415  cc 10251  2c2 11407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-12 2222  ax-ext 2804  ax-1cn 10311  ax-addcl 10313
This theorem depends on definitions:  df-bi 199  df-an 387  df-tru 1662  df-ex 1881  df-sb 2070  df-clab 2813  df-cleq 2819  df-clel 2822  df-v 3417  df-2 11415
This theorem is referenced by:  fzprval  12696  fztpval  12697  funcnvs3  14036  funcnvs4  14037  wrd3tpop  14070  wrdl3s3  14085  pmtrprfval  18258  m2detleiblem3  20804  m2detleiblem4  20805  ehl2eudis  23591  iblcnlem1  23954  gausslemma2dlem4  25508  2lgslem4  25545  selberglem1  25648  axlowdimlem4  26245  2wlkdlem4  27258  2pthdlem1  27260  umgrwwlks2on  27287  3wlkdlem4  27539  3wlkdlem5  27540  3pthdlem1  27541  3wlkdlem10  27546  upgr3v3e3cycl  27557  upgr4cycl4dv4e  27562  eulerpathpr  27618  ex-ima  27858  prodfzo03  31231  circlevma  31270  circlemethhgt  31271  hgt750lemg  31282  hgt750lemb  31284  hgt750lema  31285  hgt750leme  31286  tgoldbachgtde  31288  tgoldbachgt  31291  rabren3dioph  38224  refsum2cnlem1  40015  nnsum3primes4  42507  nnsum3primesgbe  42511  nnsum4primesodd  42515  nnsum4primesoddALTV  42516  zlmodzxzldeplem3  43139  zlmodzxzldeplem4  43140  fv2prop  43269  rrx2pyel  43293  prelrrx2  43294  rrx2line  43295  rrx2linest  43297  rrx2linesl  43298  2sphere0  43303  line2ylem  43304  line2  43305  line2x  43307  line2y  43308
  Copyright terms: Public domain W3C validator