Theorem 1ex 11146

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ℂcc 11042  1c1 11045

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 11102

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 3446

This theorem is referenced by:  1nn  12173  dfnn2  12175  nn1suc  12184  nn0ind-raph  12610  fzprval  13522  fztpval  13523  expval  14004  m1expcl2  14026  1exp  14032  facnn  14216  fac0  14217  prhash2ex  14340  funcnvs2  14855  funcnvs3  14856  funcnvs4  14857  wrdlen2i  14884  wrd2pr2op  14885  wrd3tpop  14890  wwlktovf1  14899  wrdl3s3  14904  relexp1g  14968  dfid6  14970  sgnval  15030  harmonic  15801  prodf1f  15834  fprodntriv  15884  prod1  15886  fprodss  15890  fprodn0f  15933  ege2le3  16032  ruclem8  16181  ruclem11  16184  1nprm  16625  pcmpt  16839  smndex2dnrinv  18818  mgmnsgrpex  18834  pmtrprfval  19393  pmtrprfvalrn  19394  psgnprfval  19427  psgnprfval1  19428  abvtrivd  20717  pzriprng1ALT  21382  cnmsgnsubg  21462  psdmplcl  22025  psdmul  22029  psdmvr  22032  m2detleiblem1  22487  m2detleiblem5  22488  m2detleiblem6  22489  m2detleiblem3  22492  m2detleiblem4  22493  m2detleib  22494  imasdsf1olem  24237  pcopt  24898  pcopt2  24899  pcoass  24900  ehl1eudis  25296  ehl2eudis  25298  voliunlem1  25427  i1f1lem  25566  i1f1  25567  itg11  25568  iblcnlem1  25665  bddibl  25717  dvexp  25833  dvef  25860  mvth  25873  iaa  26209  aalioulem2  26217  efrlim  26855  efrlimOLD  26856  amgmlem  26876  amgm  26877  wilthlem2  26955  wilthlem3  26956  basellem7  26973  basellem9  26975  ppiublem2  27090  pclogsum  27102  bposlem5  27175  lgsfval  27189  lgsdir2lem3  27214  lgsdir  27219  lgsdilem2  27220  lgsdi  27221  lgsne0  27222  addsqnreup  27330  ostth1  27520  istrkg2ld  28363  axlowdimlem4  28848  axlowdimlem6  28850  axlowdimlem10  28854  axlowdimlem11  28855  axlowdimlem12  28856  axlowdimlem13  28857  axlowdim1  28862  umgr2v2eedg  29428  umgr2v2e  29429  umgr2v2evd2  29431  2wlklem  29569  usgr2trlncl  29663  2wlkdlem4  29831  2wlkdlem5  29832  2pthdlem1  29833  2wlkdlem10  29838  wwlks2onv  29856  elwwlks2ons3im  29857  umgrwwlks2on  29860  3wlkdlem4  30064  3wlkdlem5  30065  3pthdlem1  30066  3wlkdlem10  30071  upgr3v3e3cycl  30082  upgr4cycl4dv4e  30087  konigsberglem4  30157  konigsberglem5  30158  ex-xp  30338  nmopun  31916  pjnmopi  32050  iuninc  32462  fprodex01  32723  sgncl  32729  s2rnOLD  32838  s3rnOLD  32840  psgnid  33027  cyc3fv2  33068  cnmsgn0g  33076  cyc3evpm  33080  sgnsval  33091  sgnsf  33092  1fldgenq  33245  constrconj  33708  nn0constr  33724  cntnevol  34191  ddeval1  34197  ddeval0  34198  eulerpartgbij  34336  coinfliprv  34447  prodfzo03  34567  circlevma  34606  circlemethhgt  34607  hgt750lemg  34618  hgt750lemb  34620  hgt750lema  34621  hgt750leme  34622  tgoldbachgtde  34624  tgoldbachgt  34627  subfacp1lem1  35139  subfacp1lem2a  35140  subfacp1lem3  35142  subfacp1lem5  35144  cvmliftlem10  35254  sinccvglem  35632  poimirlem1  37588  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem10  37597  poimirlem11  37598  poimirlem12  37599  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem28  37615  poimirlem29  37616  poimirlem31  37618  itg2addnclem  37638  sticksstones11  42117  readvrec  42323  rabren3dioph  42776  2nn0ind  42907  flcidc  43132  dfrcl4  43638  fvilbdRP  43652  fvrcllb1d  43657  iunrelexp0  43664  corclrcl  43669  relexp1idm  43676  cotrcltrcl  43687  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  dvsid  44293  binomcxplemnotnn0  44318  refsum2cnlem1  45004  infleinf  45341  itgsin0pilem1  45921  fourierdlem29  46107  fourierdlem56  46133  fourierdlem62  46139  fourierswlem  46201  fouriersw  46202  lamberte  46862  cjnpoly  46863  fun2dmnopgexmpl  47258  sbgoldbo  47761  nnsum3primes4  47762  nnsum3primesgbe  47766  nnsum4primesodd  47770  nnsum4primesoddALTV  47771  cycl3grtrilem  47918  stgr1  47933  usgrexmpl1lem  47985  usgrexmpl1tri  47989  usgrexmpl2lem  47990  usgrexmpl2nb0  47995  usgrexmpl2nb1  47996  usgrexmpl2nb2  47997  usgrexmpl2trifr  48001  gpgiedgdmellem  48010  gpgvtx1  48018  opgpgvtx  48019  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  gpgedgiov  48029  gpgedg2iv  48031  gpg5nbgrvtx03starlem1  48032  gpg5nbgrvtx03starlem3  48034  gpg5nbgrvtx13starlem1  48035  gpg5nbgrvtx13starlem2  48036  gpg5nbgrvtx13starlem3  48037  gpg3nbgrvtx0  48040  gpg3nbgrvtx0ALT  48041  gpg3nbgrvtx1  48042  gpgcubic  48043  gpg5nbgr3star  48045  gpg3kgrtriex  48053  gpgprismgr4cycllem2  48059  gpgprismgr4cycllem3  48060  gpgprismgr4cycllem7  48064  gpgprismgr4cycllem9  48066  pgnioedg1  48071  pgnioedg2  48072  pgnioedg3  48073  pgnioedg4  48074  pgnioedg5  48075  pgnbgreunbgrlem2lem1  48077  pgnbgreunbgrlem2lem2  48078  pgnbgreunbgrlem2lem3  48079  pgnbgreunbgrlem2  48080  pgnbgreunbgrlem3  48081  pgnbgreunbgrlem4  48082  pgnbgreunbgrlem5lem1  48083  pgnbgreunbgrlem5lem2  48084  pgnbgreunbgrlem5lem3  48085  pgnbgreunbgrlem6  48087  zlmodzxzel  48316  zlmodzxz0  48317  zlmodzxzscm  48318  zlmodzxzadd  48319  blenval  48533  nn0sumshdiglemB  48582  fv2arycl  48610  2arympt  48611  2arymptfv  48612  2arymaptf1  48615  2arymaptfo  48616  fv1prop  48661  rrx2pxel  48673  prelrrx2  48675  prelrrx2b  48676  rrx2pnecoorneor  48677  rrx2xpref1o  48680  rrx2plordisom  48685  ehl2eudisval0  48687  rrx2line  48702  rrx2linest  48704  rrx2linesl  48705  2sphere0  48712  line2ylem  48713  line2  48714  line2xlem  48715  line2x  48716  line2y  48717  itscnhlinecirc02p  48747  inlinecirc02plem  48748