Theorem 1ex 11130

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 11086	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 3461	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3438  ℂcc 11026  1c1 11029

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-1cn 11086

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440

This theorem is referenced by:  1nn  12158  dfnn2  12160  nn1suc  12169  nn0ind-raph  12595  fzprval  13507  fztpval  13508  expval  13989  m1expcl2  14011  1exp  14017  facnn  14201  fac0  14202  prhash2ex  14325  funcnvs2  14839  funcnvs3  14840  funcnvs4  14841  wrdlen2i  14868  wrd2pr2op  14869  wrd3tpop  14874  wwlktovf1  14883  wrdl3s3  14888  relexp1g  14952  dfid6  14954  sgnval  15014  harmonic  15785  prodf1f  15818  fprodntriv  15868  prod1  15870  fprodss  15874  fprodn0f  15917  ege2le3  16016  ruclem8  16165  ruclem11  16168  1nprm  16609  pcmpt  16823  smndex2dnrinv  18808  mgmnsgrpex  18824  pmtrprfval  19385  pmtrprfvalrn  19386  psgnprfval  19419  psgnprfval1  19420  abvtrivd  20736  pzriprng1ALT  21422  cnmsgnsubg  21503  psdmplcl  22066  psdmul  22070  psdmvr  22073  m2detleiblem1  22528  m2detleiblem5  22529  m2detleiblem6  22530  m2detleiblem3  22533  m2detleiblem4  22534  m2detleib  22535  imasdsf1olem  24278  pcopt  24939  pcopt2  24940  pcoass  24941  ehl1eudis  25337  ehl2eudis  25339  voliunlem1  25468  i1f1lem  25607  i1f1  25608  itg11  25609  iblcnlem1  25706  bddibl  25758  dvexp  25874  dvef  25901  mvth  25914  iaa  26250  aalioulem2  26258  efrlim  26896  efrlimOLD  26897  amgmlem  26917  amgm  26918  wilthlem2  26996  wilthlem3  26997  basellem7  27014  basellem9  27016  ppiublem2  27131  pclogsum  27143  bposlem5  27216  lgsfval  27230  lgsdir2lem3  27255  lgsdir  27260  lgsdilem2  27261  lgsdi  27262  lgsne0  27263  addsqnreup  27371  ostth1  27561  istrkg2ld  28424  axlowdimlem4  28909  axlowdimlem6  28911  axlowdimlem10  28915  axlowdimlem11  28916  axlowdimlem12  28917  axlowdimlem13  28918  axlowdim1  28923  umgr2v2eedg  29489  umgr2v2e  29490  umgr2v2evd2  29492  2wlklem  29630  usgr2trlncl  29724  2wlkdlem4  29892  2wlkdlem5  29893  2pthdlem1  29894  2wlkdlem10  29899  wwlks2onv  29917  elwwlks2ons3im  29918  umgrwwlks2on  29921  3wlkdlem4  30125  3wlkdlem5  30126  3pthdlem1  30127  3wlkdlem10  30132  upgr3v3e3cycl  30143  upgr4cycl4dv4e  30148  konigsberglem4  30218  konigsberglem5  30219  ex-xp  30399  nmopun  31977  pjnmopi  32111  iuninc  32523  fprodex01  32789  sgncl  32795  s2rnOLD  32904  s3rnOLD  32906  psgnid  33058  cyc3fv2  33099  cnmsgn0g  33107  cyc3evpm  33111  sgnsval  33122  sgnsf  33123  1fldgenq  33280  constrconj  33731  nn0constr  33747  cntnevol  34214  ddeval1  34220  ddeval0  34221  eulerpartgbij  34359  coinfliprv  34470  prodfzo03  34590  circlevma  34629  circlemethhgt  34630  hgt750lemg  34641  hgt750lemb  34643  hgt750lema  34644  hgt750leme  34645  tgoldbachgtde  34647  tgoldbachgt  34650  subfacp1lem1  35171  subfacp1lem2a  35172  subfacp1lem3  35174  subfacp1lem5  35176  cvmliftlem10  35286  sinccvglem  35664  poimirlem1  37620  poimirlem2  37621  poimirlem3  37622  poimirlem4  37623  poimirlem6  37625  poimirlem7  37626  poimirlem10  37629  poimirlem11  37630  poimirlem12  37631  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem23  37642  poimirlem24  37643  poimirlem25  37644  poimirlem28  37647  poimirlem29  37648  poimirlem31  37650  itg2addnclem  37670  sticksstones11  42149  readvrec  42355  rabren3dioph  42808  2nn0ind  42938  flcidc  43163  dfrcl4  43669  fvilbdRP  43683  fvrcllb1d  43688  iunrelexp0  43695  corclrcl  43700  relexp1idm  43707  cotrcltrcl  43718  trclfvdecomr  43721  corcltrcl  43732  cotrclrcl  43735  dvsid  44324  binomcxplemnotnn0  44349  refsum2cnlem1  45035  infleinf  45371  itgsin0pilem1  45951  fourierdlem29  46137  fourierdlem56  46163  fourierdlem62  46169  fourierswlem  46231  fouriersw  46232  lamberte  46892  cjnpoly  46893  fun2dmnopgexmpl  47288  sbgoldbo  47791  nnsum3primes4  47792  nnsum3primesgbe  47796  nnsum4primesodd  47800  nnsum4primesoddALTV  47801  cycl3grtrilem  47950  stgr1  47965  usgrexmpl1lem  48025  usgrexmpl1tri  48029  usgrexmpl2lem  48030  usgrexmpl2nb0  48035  usgrexmpl2nb1  48036  usgrexmpl2nb2  48037  usgrexmpl2trifr  48041  gpgiedgdmellem  48050  gpgvtx1  48058  opgpgvtx  48059  gpgedgvtx1  48066  gpgvtxedg0  48067  gpgvtxedg1  48068  gpgedgiov  48069  gpgedg2iv  48071  gpg5nbgrvtx03starlem1  48072  gpg5nbgrvtx03starlem3  48074  gpg5nbgrvtx13starlem1  48075  gpg5nbgrvtx13starlem2  48076  gpg5nbgrvtx13starlem3  48077  gpg3nbgrvtx0  48080  gpg3nbgrvtx0ALT  48081  gpg3nbgrvtx1  48082  gpgcubic  48083  gpg5nbgr3star  48085  gpg3kgrtriex  48093  gpgprismgr4cycllem2  48100  gpgprismgr4cycllem3  48101  gpgprismgr4cycllem7  48105  gpgprismgr4cycllem9  48107  pgnioedg1  48112  pgnioedg2  48113  pgnioedg3  48114  pgnioedg4  48115  pgnioedg5  48116  pgnbgreunbgrlem2lem1  48118  pgnbgreunbgrlem2lem2  48119  pgnbgreunbgrlem2lem3  48120  pgnbgreunbgrlem2  48121  pgnbgreunbgrlem3  48122  pgnbgreunbgrlem4  48123  pgnbgreunbgrlem5lem1  48124  pgnbgreunbgrlem5lem2  48125  pgnbgreunbgrlem5lem3  48126  pgnbgreunbgrlem6  48128  gpg5edgnedg  48134  grlimedgnedg  48135  zlmodzxzel  48359  zlmodzxz0  48360  zlmodzxzscm  48361  zlmodzxzadd  48362  blenval  48576  nn0sumshdiglemB  48625  fv2arycl  48653  2arympt  48654  2arymptfv  48655  2arymaptf1  48658  2arymaptfo  48659  fv1prop  48704  rrx2pxel  48716  prelrrx2  48718  prelrrx2b  48719  rrx2pnecoorneor  48720  rrx2xpref1o  48723  rrx2plordisom  48728  ehl2eudisval0  48730  rrx2line  48745  rrx2linest  48747  rrx2linesl  48748  2sphere0  48755  line2ylem  48756  line2  48757  line2xlem  48758  line2x  48759  line2y  48760  itscnhlinecirc02p  48790  inlinecirc02plem  48791