Theorem 1ex 10980

Description: One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1ex	⊢ 1 ∈ V

Proof of Theorem 1ex

Step	Hyp	Ref	Expression
1		ax-1cn 10938	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 3452	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 2107  Vcvv 3433  ℂcc 10878  1c1 10881

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 2710  ax-1cn 10938

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435

This theorem is referenced by:  1nn  11993  dfnn2  11995  nn1suc  12004  nn0ind-raph  12429  fzprval  13326  fztpval  13327  expval  13793  m1expcl2  13813  1exp  13821  facnn  13998  fac0  13999  prhash2ex  14123  funcnvs2  14635  funcnvs3  14636  funcnvs4  14637  wrdlen2i  14664  wrd2pr2op  14665  wrd3tpop  14670  wwlktovf1  14681  wrdl3s3  14686  relexp1g  14746  dfid6  14748  sgnval  14808  harmonic  15580  prodf1f  15613  fprodntriv  15661  prod1  15663  fprodss  15667  fprodn0f  15710  ege2le3  15808  ruclem8  15955  ruclem11  15958  1nprm  16393  pcmpt  16602  smndex2dnrinv  18563  mgmnsgrpex  18579  pmtrprfval  19104  pmtrprfvalrn  19105  psgnprfval  19138  psgnprfval1  19139  abvtrivd  20109  cnmsgnsubg  20791  m2detleiblem1  21782  m2detleiblem5  21783  m2detleiblem6  21784  m2detleiblem3  21787  m2detleiblem4  21788  m2detleib  21789  imasdsf1olem  23535  pcopt  24194  pcopt2  24195  pcoass  24196  ehl1eudis  24593  ehl2eudis  24595  voliunlem1  24723  i1f1lem  24862  i1f1  24863  itg11  24864  iblcnlem1  24961  bddibl  25013  dvexp  25126  dvef  25153  mvth  25165  iaa  25494  aalioulem2  25502  efrlim  26128  amgmlem  26148  amgm  26149  wilthlem2  26227  wilthlem3  26228  basellem7  26245  basellem9  26247  ppiublem2  26360  pclogsum  26372  bposlem5  26445  lgsfval  26459  lgsdir2lem3  26484  lgsdir  26489  lgsdilem2  26490  lgsdi  26491  lgsne0  26492  addsqnreup  26600  ostth1  26790  istrkg2ld  26830  axlowdimlem4  27322  axlowdimlem6  27324  axlowdimlem10  27328  axlowdimlem11  27329  axlowdimlem12  27330  axlowdimlem13  27331  axlowdim1  27336  umgr2v2eedg  27900  umgr2v2e  27901  umgr2v2evd2  27903  2wlklem  28044  usgr2trlncl  28137  2wlkdlem4  28302  2wlkdlem5  28303  2pthdlem1  28304  2wlkdlem10  28309  wwlks2onv  28327  elwwlks2ons3im  28328  umgrwwlks2on  28331  3wlkdlem4  28535  3wlkdlem5  28536  3pthdlem1  28537  3wlkdlem10  28542  upgr3v3e3cycl  28553  upgr4cycl4dv4e  28558  konigsberglem4  28628  konigsberglem5  28629  ex-xp  28809  nmopun  30385  pjnmopi  30519  iuninc  30909  fprodex01  31148  s2rn  31227  s3rn  31229  psgnid  31373  cyc3fv2  31414  cnmsgn0g  31422  cyc3evpm  31426  sgnsval  31437  sgnsf  31438  cntnevol  32205  ddeval1  32211  ddeval0  32212  eulerpartgbij  32348  coinfliprv  32458  sgncl  32514  prodfzo03  32592  circlevma  32631  circlemethhgt  32632  hgt750lemg  32643  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  tgoldbachgtde  32649  tgoldbachgt  32652  subfacp1lem1  33150  subfacp1lem2a  33151  subfacp1lem3  33153  subfacp1lem5  33155  cvmliftlem10  33265  sinccvglem  33639  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem10  35796  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem24  35810  poimirlem25  35811  poimirlem28  35814  poimirlem29  35815  poimirlem31  35817  itg2addnclem  35837  sticksstones11  40119  rabren3dioph  40644  2nn0ind  40774  flcidc  41006  dfrcl4  41291  fvilbdRP  41305  fvrcllb1d  41310  iunrelexp0  41317  corclrcl  41322  relexp1idm  41329  cotrcltrcl  41340  trclfvdecomr  41343  corcltrcl  41354  cotrclrcl  41357  dvsid  41956  binomcxplemnotnn0  41981  refsum2cnlem1  42587  infleinf  42918  itgsin0pilem1  43498  fourierdlem29  43684  fourierdlem56  43710  fourierdlem62  43716  fourierswlem  43778  fouriersw  43779  fun2dmnopgexmpl  44787  sbgoldbo  45250  nnsum3primes4  45251  nnsum3primesgbe  45255  nnsum4primesodd  45259  nnsum4primesoddALTV  45260  zlmodzxzel  45702  zlmodzxz0  45703  zlmodzxzscm  45704  zlmodzxzadd  45705  blenval  45928  nn0sumshdiglemB  45977  fv2arycl  46005  2arympt  46006  2arymptfv  46007  2arymaptf1  46010  2arymaptfo  46011  fv1prop  46056  rrx2pxel  46068  prelrrx2  46070  prelrrx2b  46071  rrx2pnecoorneor  46072  rrx2xpref1o  46075  rrx2plordisom  46080  ehl2eudisval0  46082  rrx2line  46097  rrx2linest  46099  rrx2linesl  46100  2sphere0  46107  line2ylem  46108  line2  46109  line2xlem  46110  line2x  46111  line2y  46112  itscnhlinecirc02p  46142  inlinecirc02plem  46143