Theorem 1ex 11140

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ℂcc 11036  1c1 11039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444

This theorem is referenced by:  1nn  12168  dfnn2  12170  nn1suc  12179  nn0ind-raph  12604  fzprval  13513  fztpval  13514  expval  13998  m1expcl2  14020  1exp  14026  facnn  14210  fac0  14211  prhash2ex  14334  funcnvs2  14848  funcnvs3  14849  funcnvs4  14850  wrdlen2i  14877  wrd2pr2op  14878  wrd3tpop  14883  wwlktovf1  14892  wrdl3s3  14897  relexp1g  14961  dfid6  14963  sgnval  15023  harmonic  15794  prodf1f  15827  fprodntriv  15877  prod1  15879  fprodss  15883  fprodn0f  15926  ege2le3  16025  ruclem8  16174  ruclem11  16177  1nprm  16618  pcmpt  16832  smndex2dnrinv  18852  mgmnsgrpex  18868  pmtrprfval  19428  pmtrprfvalrn  19429  psgnprfval  19462  psgnprfval1  19463  abvtrivd  20777  pzriprng1ALT  21463  cnmsgnsubg  21544  psdmplcl  22117  psdmul  22121  psdmvr  22124  m2detleiblem1  22580  m2detleiblem5  22581  m2detleiblem6  22582  m2detleiblem3  22585  m2detleiblem4  22586  m2detleib  22587  imasdsf1olem  24329  pcopt  24990  pcopt2  24991  pcoass  24992  ehl1eudis  25388  ehl2eudis  25390  voliunlem1  25519  i1f1lem  25658  i1f1  25659  itg11  25660  iblcnlem1  25757  bddibl  25809  dvexp  25925  dvef  25952  mvth  25965  iaa  26301  aalioulem2  26309  efrlim  26947  efrlimOLD  26948  amgmlem  26968  amgm  26969  wilthlem2  27047  wilthlem3  27048  basellem7  27065  basellem9  27067  ppiublem2  27182  pclogsum  27194  bposlem5  27267  lgsfval  27281  lgsdir2lem3  27306  lgsdir  27311  lgsdilem2  27312  lgsdi  27313  lgsne0  27314  addsqnreup  27422  ostth1  27612  istrkg2ld  28544  axlowdimlem4  29030  axlowdimlem6  29032  axlowdimlem10  29036  axlowdimlem11  29037  axlowdimlem12  29038  axlowdimlem13  29039  axlowdim1  29044  umgr2v2eedg  29610  umgr2v2e  29611  umgr2v2evd2  29613  2wlklem  29751  usgr2trlncl  29845  2wlkdlem4  30013  2wlkdlem5  30014  2pthdlem1  30015  2wlkdlem10  30020  wwlks2onv  30038  elwwlks2ons3im  30039  usgrwwlks2on  30043  umgrwwlks2on  30044  3wlkdlem4  30249  3wlkdlem5  30250  3pthdlem1  30251  3wlkdlem10  30256  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  konigsberglem4  30342  konigsberglem5  30343  ex-xp  30523  nmopun  32102  pjnmopi  32236  iuninc  32647  fprodex01  32917  sgncl  32923  s2rnOLD  33037  s3rnOLD  33039  psgnid  33191  cyc3fv2  33232  cnmsgn0g  33240  cyc3evpm  33244  sgnsval  33255  sgnsf  33256  1fldgenq  33416  gsumind  33438  esplyfvaln  33751  constrconj  33923  nn0constr  33939  cntnevol  34406  ddeval1  34412  ddeval0  34413  eulerpartgbij  34550  coinfliprv  34661  prodfzo03  34781  circlevma  34820  circlemethhgt  34821  hgt750lemg  34832  hgt750lemb  34834  hgt750lema  34835  hgt750leme  34836  tgoldbachgtde  34838  tgoldbachgt  34841  subfacp1lem1  35395  subfacp1lem2a  35396  subfacp1lem3  35398  subfacp1lem5  35400  cvmliftlem10  35510  sinccvglem  35888  poimirlem1  37872  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem10  37881  poimirlem11  37882  poimirlem12  37883  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem28  37899  poimirlem29  37900  poimirlem31  37902  itg2addnclem  37922  sticksstones11  42526  readvrec  42732  rabren3dioph  43172  2nn0ind  43302  flcidc  43527  dfrcl4  44032  fvilbdRP  44046  fvrcllb1d  44051  iunrelexp0  44058  corclrcl  44063  relexp1idm  44070  cotrcltrcl  44081  trclfvdecomr  44084  corcltrcl  44095  cotrclrcl  44098  dvsid  44687  binomcxplemnotnn0  44712  refsum2cnlem1  45397  infleinf  45730  itgsin0pilem1  46308  fourierdlem29  46494  fourierdlem56  46520  fourierdlem62  46526  fourierswlem  46588  fouriersw  46589  nthrucw  47244  lamberte  47248  cjnpoly  47249  fun2dmnopgexmpl  47644  sbgoldbo  48147  nnsum3primes4  48148  nnsum3primesgbe  48152  nnsum4primesodd  48156  nnsum4primesoddALTV  48157  cycl3grtrilem  48306  stgr1  48321  usgrexmpl1lem  48381  usgrexmpl1tri  48385  usgrexmpl2lem  48386  usgrexmpl2nb0  48391  usgrexmpl2nb1  48392  usgrexmpl2nb2  48393  usgrexmpl2trifr  48397  gpgiedgdmellem  48406  gpgvtx1  48414  opgpgvtx  48415  gpgedgvtx1  48422  gpgvtxedg0  48423  gpgvtxedg1  48424  gpgedgiov  48425  gpgedg2iv  48427  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg3nbgrvtx0  48436  gpg3nbgrvtx0ALT  48437  gpg3nbgrvtx1  48438  gpgcubic  48439  gpg5nbgr3star  48441  gpg3kgrtriex  48449  gpgprismgr4cycllem2  48456  gpgprismgr4cycllem3  48457  gpgprismgr4cycllem7  48461  gpgprismgr4cycllem9  48463  pgnioedg1  48468  pgnioedg2  48469  pgnioedg3  48470  pgnioedg4  48471  pgnioedg5  48472  pgnbgreunbgrlem2lem1  48474  pgnbgreunbgrlem2lem2  48475  pgnbgreunbgrlem2lem3  48476  pgnbgreunbgrlem2  48477  pgnbgreunbgrlem3  48478  pgnbgreunbgrlem4  48479  pgnbgreunbgrlem5lem1  48480  pgnbgreunbgrlem5lem2  48481  pgnbgreunbgrlem5lem3  48482  pgnbgreunbgrlem6  48484  gpg5edgnedg  48490  grlimedgnedg  48491  zlmodzxzel  48715  zlmodzxz0  48716  zlmodzxzscm  48717  zlmodzxzadd  48718  blenval  48931  nn0sumshdiglemB  48980  fv2arycl  49008  2arympt  49009  2arymptfv  49010  2arymaptf1  49013  2arymaptfo  49014  fv1prop  49059  rrx2pxel  49071  prelrrx2  49073  prelrrx2b  49074  rrx2pnecoorneor  49075  rrx2xpref1o  49078  rrx2plordisom  49083  ehl2eudisval0  49085  rrx2line  49100  rrx2linest  49102  rrx2linesl  49103  2sphere0  49110  line2ylem  49111  line2  49112  line2xlem  49113  line2x  49114  line2y  49115  itscnhlinecirc02p  49145  inlinecirc02plem  49146