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

Theorem 1ex 10318
Description: One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1ex 1 ∈ V

Proof of Theorem 1ex
StepHypRef Expression
1 ax-1cn 10276 . 2 1 ∈ ℂ
21elexi 3406 1 1 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2158  Vcvv 3390  cc 10216  1c1 10219
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-12 2216  ax-ext 2784  ax-1cn 10276
This theorem depends on definitions:  df-bi 198  df-an 385  df-tru 1641  df-ex 1860  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-v 3392
This theorem is referenced by:  1nn  11313  dfnn2  11315  nn1suc  11323  nn0ind-raph  11739  fzprval  12620  fztpval  12621  expval  13081  m1expcl2  13101  1exp  13108  facnn  13278  fac0  13279  prhash2ex  13400  funcnvs2  13878  funcnvs3  13879  funcnvs4  13880  wrdlen2i  13907  wrd2pr2op  13908  wrd3tpop  13912  wwlktovf1  13921  wrdl3s3  13926  relexp1g  13985  dfid6  13987  sgnval  14047  harmonic  14809  prodf1f  14841  fprodntriv  14889  prod1  14891  fprodss  14895  fprodn0f  14938  ege2le3  15036  ruclem8  15182  ruclem11  15185  1nprm  15606  pcmpt  15809  mgmnsgrpex  17619  pmtrprfval  18104  pmtrprfvalrn  18105  psgnprfval  18138  psgnprfval1  18139  abvtrivd  19040  cnmsgnsubg  20126  m2detleiblem1  20637  m2detleiblem5  20638  m2detleiblem6  20639  m2detleiblem3  20642  m2detleiblem4  20643  m2detleib  20644  imasdsf1olem  22387  pcopt  23030  pcopt2  23031  pcoass  23032  voliunlem1  23527  i1f1lem  23666  i1f1  23667  itg11  23668  iblcnlem1  23764  bddibl  23816  dvexp  23926  mvth  23965  iaa  24290  aalioulem2  24298  efrlim  24906  amgmlem  24926  amgm  24927  wilthlem2  25005  wilthlem3  25006  basellem7  25023  basellem9  25025  ppiublem2  25138  pclogsum  25150  bposlem5  25223  lgsfval  25237  lgsdir2lem3  25262  lgsdir  25267  lgsdilem2  25268  lgsdi  25269  lgsne0  25270  ostth1  25532  istrkg2ld  25569  axlowdimlem4  26035  axlowdimlem6  26037  axlowdimlem10  26041  axlowdimlem11  26042  axlowdimlem12  26043  axlowdimlem13  26044  axlowdim1  26049  umgr2v2eedg  26644  umgr2v2e  26645  umgr2v2evd2  26647  2wlklem  26787  usgr2trlncl  26880  2wlkdlem4  27064  2wlkdlem5  27065  2pthdlem1  27066  2wlkdlem10  27071  wwlks2onv  27089  elwwlks2ons3im  27090  elwwlks2ons3OLD  27092  umgrwwlks2on  27094  3wlkdlem4  27331  3wlkdlem5  27332  3pthdlem1  27333  3wlkdlem10  27338  upgr3v3e3cycl  27349  upgr4cycl4dv4e  27354  konigsberglem4  27424  konigsberglem5  27425  ex-xp  27620  nmopun  29198  pjnmopi  29332  iuninc  29701  fprodex01  29895  sgnsval  30050  sgnsf  30051  psgnid  30169  cntnevol  30613  ddeval1  30619  ddeval0  30620  eulerpartgbij  30756  coinfliprv  30866  sgncl  30922  prodfzo03  31003  circlevma  31042  circlemethhgt  31043  hgt750lemg  31054  hgt750lemb  31056  hgt750lema  31057  hgt750leme  31058  tgoldbachgtde  31060  tgoldbachgt  31063  subfacp1lem1  31481  subfacp1lem2a  31482  subfacp1lem3  31484  subfacp1lem5  31486  cvmliftlem10  31596  sinccvglem  31885  poimirlem1  33720  poimirlem2  33721  poimirlem3  33722  poimirlem4  33723  poimirlem6  33725  poimirlem7  33726  poimirlem10  33729  poimirlem11  33730  poimirlem12  33731  poimirlem16  33735  poimirlem17  33736  poimirlem19  33738  poimirlem20  33739  poimirlem23  33742  poimirlem24  33743  poimirlem25  33744  poimirlem28  33747  poimirlem29  33748  poimirlem31  33750  itg2addnclem  33770  rabren3dioph  37878  2nn0ind  38008  flcidc  38242  dfrcl4  38465  fvilbdRP  38479  fvrcllb1d  38484  iunrelexp0  38491  corclrcl  38496  relexp1idm  38503  cotrcltrcl  38514  trclfvdecomr  38517  corcltrcl  38528  cotrclrcl  38531  dvsid  39027  binomcxplemnotnn0  39052  refsum2cnlem1  39687  infleinf  40065  itgsin0pilem1  40642  fourierdlem29  40829  fourierdlem56  40855  fourierdlem62  40861  fourierswlem  40923  fouriersw  40924  fun2dmnopgexmpl  41871  sbgoldbo  42247  nnsum3primes4  42248  nnsum3primesgbe  42252  nnsum4primesodd  42256  nnsum4primesoddALTV  42257  zlmodzxzel  42698  zlmodzxz0  42699  zlmodzxzscm  42700  zlmodzxzadd  42701  blenval  42930  nn0sumshdiglemB  42979
  Copyright terms: Public domain W3C validator