Theorem 1ex 11340

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ℂcc 11235  1c1 11238

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-1cn 11295

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456

This theorem is used by:  1elpr01  11341  1nn  12384  dfnn2  12386  nn1suc  12395  1eltp012  12451  nn0ind-raph  12837  fzprval  13757  fztpval  13758  expval  14244  m1expcl2  14266  1exp  14272  facnn  14458  fac0  14459  prhash2ex  14582  funcnvs2  15105  funcnvs3  15106  funcnvs4  15107  wrdlen2i  15134  wrd2pr2op  15135  wrd3tpop  15140  wwlktovf1  15151  relexp1g  15220  dfid6  15222  sgnval  15282  sgndm  15290  sgncl  15291  harmonic  16069  prodf1f  16102  fprodntriv  16150  prod1  16152  fprodss  16156  fprodn0f  16199  ege2le3  16297  ruclem8  16446  ruclem11  16449  1nprm  16895  pcmpt  17111  smndex2dnrinv  19155  mgmnsgrpex  19171  pmtrprfval  19743  pmtrprfvalrn  19744  psgnprfval  19777  psgnprfval1  19778  abvtrivd  21131  pzriprng1ALT  21846  cnmsgnsubg  21927  psdmplcl  22527  psdmul  22531  psdmvr  22534  m2detleiblem1  22983  m2detleiblem5  22984  m2detleiblem6  22985  m2detleiblem3  22988  m2detleiblem4  22989  m2detleib  22990  imasdsf1olem  24736  pcopt  25387  pcopt2  25388  pcoass  25389  ehl2eudis  25787  voliunlem1  25915  i1f1lem  26054  itg11  26056  iblcnlem1  26152  bddibl  26204  dvexp  26317  dvef  26344  mvth  26356  iaaOLD  26698  aalioulem2  26706  efrlim  27343  amgmlem  27363  amgm  27364  wilthlem2  27442  wilthlem3  27443  basellem7  27460  basellem9  27462  ppiublem2  27576  pclogsum  27588  bposlem5  27661  lgsfval  27675  lgsdir2lem3  27700  lgsdir  27705  lgsdilem2  27706  lgsdi  27707  lgsne0  27708  addsqnreup  27816  ostth1  28006  istrkg2ld  28968  axlowdimlem4  29569  axlowdimlem6  29571  axlowdimlem10  29575  axlowdimlem11  29576  axlowdimlem12  29577  axlowdimlem13  29578  axlowdim1  29583  umgr2v2eedg  30151  umgr2v2e  30152  umgr2v2evd2  30154  2wlklem  30292  usgr2trlncl  30392  2wlkdlem4  30563  2wlkdlem5  30564  2pthdlem1  30565  2wlkdlem10  30570  3wlkdlem4  30809  3wlkdlem5  30810  3pthdlem1  30811  3wlkdlem10  30816  upgr3v3e3cycl  30827  upgr4cycl4dv4e  30832  konigsberglem4  30902  konigsberglem5  30903  ex-xp  31083  nmopun  32662  pjnmopi  32796  iuninc  33243  fprodex01  33502  psgnid  33747  cnmsgn0g  33796  cyc3evpm  33800  sgnsval  33811  sgnsf  33812  1fldgenq  33981  gsumind  34003  cntnevol  34965  ddeval1  34971  ddeval0  34972  eulerpartgbij  35108  coinfliprv  35219  hgt750lemg  35387  hgt750lemb  35389  tgoldbachgt  35396  subfacp1lem1  36145  subfacp1lem2a  36146  subfacp1lem3  36148  subfacp1lem5  36150  cvmliftlem10  36260  sinccvglem  36638  poimirlem1  38800  poimirlem2  38801  poimirlem3  38802  poimirlem4  38803  poimirlem6  38805  poimirlem7  38806  poimirlem10  38809  poimirlem11  38810  poimirlem12  38811  poimirlem16  38815  poimirlem17  38816  poimirlem19  38818  poimirlem20  38819  poimirlem23  38822  poimirlem24  38823  poimirlem25  38824  poimirlem28  38827  poimirlem29  38828  poimirlem31  38830  itg2addnclem  38850  sticksstones11  43465  readvrec  43673  rabren3dioph  44082  2nn0ind  44212  flcidc  44427  dfrcl4  44931  fvilbdRP  44945  iunrelexp0  44957  corclrcl  44962  cotrcltrcl  44980  trclfvdecomr  44983  corcltrcl  44994  cotrclrcl  44997  dvsid  45570  binomcxplemnotnn0  45595  refsum2cnlem1  46322  infleinf  46650  itgsin0pilem1  47227  fourierdlem29  47413  fourierdlem56  47439  fourierdlem62  47445  fourierswlem  47507  fouriersw  47508  numtowerdt  48183  lamberte  48205  cjnpoly  48206  fun2dmnopgexmpl  48621  sbgoldbo  49152  nnsum3primes4  49153  nnsum3primesgbe  49157  nnsum4primesodd  49161  nnsum4primesoddALTV  49162  cycl3grtrilem  49311  stgr1  49326  usgrexmpl1lem  49386  usgrexmpl2lem  49391  usgrexmpl2nb0  49396  usgrexmpl2nb2  49398  usgrexmpl2trifr  49402  opgpgvtx  49420  gpgedgvtx1  49427  gpgvtxedg0  49428  gpgvtxedg1  49429  gpgedgiov  49430  gpgedg2iv  49432  gpg5nbgrvtx03starlem1  49433  gpg5nbgrvtx03starlem3  49435  gpg5nbgrvtx13starlem1  49436  gpg5nbgrvtx13starlem2  49437  gpg5nbgrvtx13starlem3  49438  gpg3nbgrvtx0  49441  gpg3nbgrvtx0ALT  49442  gpg3nbgrvtx1  49443  gpgcubic  49444  gpg5nbgr3star  49446  gpg3kgrtriex  49454  gpgprismgr4cycllem2  49461  gpgprismgr4cycllem7  49466  pgnioedg1  49473  pgnioedg2  49474  pgnioedg3  49475  pgnioedg4  49476  pgnioedg5  49477  pgnbgreunbgrlem2lem1  49479  pgnbgreunbgrlem2lem2  49480  pgnbgreunbgrlem2lem3  49481  pgnbgreunbgrlem2  49482  pgnbgreunbgrlem3  49483  pgnbgreunbgrlem4  49484  pgnbgreunbgrlem5lem1  49485  pgnbgreunbgrlem5lem2  49486  pgnbgreunbgrlem5lem3  49487  pgnbgreunbgrlem6  49489  gpg5edgnedg  49495  zlmodzxzel  49792  zlmodzxz0  49793  zlmodzxzscm  49794  zlmodzxzadd  49795  blenval  50008  nn0sumshdiglemB  50057  fv2arycl  50085  2arymptfv  50087  2arymaptf1  50090  2arymaptfo  50091  fv1prop  50136  rrx2pnecoorneor  50153  ehl2eudisval0  50163  rrx2line  50177  rrx2linest  50179  line2ylem  50188  line2  50189