Theorem 1ex 11129

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ℂcc 11025  1c1 11028

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 11085

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 3432

This theorem is referenced by:  1nn  12174  dfnn2  12176  nn1suc  12185  nn0ind-raph  12618  fzprval  13528  fztpval  13529  expval  14014  m1expcl2  14036  1exp  14042  facnn  14226  fac0  14227  prhash2ex  14350  funcnvs2  14864  funcnvs3  14865  funcnvs4  14866  wrdlen2i  14893  wrd2pr2op  14894  wrd3tpop  14899  wwlktovf1  14908  wrdl3s3  14913  relexp1g  14977  dfid6  14979  sgnval  15039  harmonic  15813  prodf1f  15846  fprodntriv  15896  prod1  15898  fprodss  15902  fprodn0f  15945  ege2le3  16044  ruclem8  16193  ruclem11  16196  1nprm  16637  pcmpt  16852  smndex2dnrinv  18875  mgmnsgrpex  18891  pmtrprfval  19451  pmtrprfvalrn  19452  psgnprfval  19485  psgnprfval1  19486  abvtrivd  20798  pzriprng1ALT  21484  cnmsgnsubg  21565  psdmplcl  22136  psdmul  22140  psdmvr  22143  m2detleiblem1  22597  m2detleiblem5  22598  m2detleiblem6  22599  m2detleiblem3  22602  m2detleiblem4  22603  m2detleib  22604  imasdsf1olem  24346  pcopt  24997  pcopt2  24998  pcoass  24999  ehl1eudis  25395  ehl2eudis  25397  voliunlem1  25525  i1f1lem  25664  i1f1  25665  itg11  25666  iblcnlem1  25763  bddibl  25815  dvexp  25928  dvef  25955  mvth  25967  iaa  26300  aalioulem2  26308  efrlim  26944  efrlimOLD  26945  amgmlem  26965  amgm  26966  wilthlem2  27044  wilthlem3  27045  basellem7  27062  basellem9  27064  ppiublem2  27178  pclogsum  27190  bposlem5  27263  lgsfval  27277  lgsdir2lem3  27302  lgsdir  27307  lgsdilem2  27308  lgsdi  27309  lgsne0  27310  addsqnreup  27418  ostth1  27608  istrkg2ld  28540  axlowdimlem4  29026  axlowdimlem6  29028  axlowdimlem10  29032  axlowdimlem11  29033  axlowdimlem12  29034  axlowdimlem13  29035  axlowdim1  29040  umgr2v2eedg  29606  umgr2v2e  29607  umgr2v2evd2  29609  2wlklem  29747  usgr2trlncl  29841  2wlkdlem4  30009  2wlkdlem5  30010  2pthdlem1  30011  2wlkdlem10  30016  wwlks2onv  30034  elwwlks2ons3im  30035  usgrwwlks2on  30039  umgrwwlks2on  30040  3wlkdlem4  30245  3wlkdlem5  30246  3pthdlem1  30247  3wlkdlem10  30252  upgr3v3e3cycl  30263  upgr4cycl4dv4e  30268  konigsberglem4  30338  konigsberglem5  30339  ex-xp  30519  nmopun  32098  pjnmopi  32232  iuninc  32643  fprodex01  32911  sgncl  32917  s2rnOLD  33017  s3rnOLD  33019  psgnid  33171  cyc3fv2  33212  cnmsgn0g  33220  cyc3evpm  33224  sgnsval  33235  sgnsf  33236  1fldgenq  33396  gsumind  33418  esplyfvaln  33731  constrconj  33903  nn0constr  33919  cntnevol  34386  ddeval1  34392  ddeval0  34393  eulerpartgbij  34530  coinfliprv  34641  prodfzo03  34761  circlevma  34800  circlemethhgt  34801  hgt750lemg  34812  hgt750lemb  34814  hgt750lema  34815  hgt750leme  34816  tgoldbachgtde  34818  tgoldbachgt  34821  subfacp1lem1  35375  subfacp1lem2a  35376  subfacp1lem3  35378  subfacp1lem5  35380  cvmliftlem10  35490  sinccvglem  35868  poimirlem1  37946  poimirlem2  37947  poimirlem3  37948  poimirlem4  37949  poimirlem6  37951  poimirlem7  37952  poimirlem10  37955  poimirlem11  37956  poimirlem12  37957  poimirlem16  37961  poimirlem17  37962  poimirlem19  37964  poimirlem20  37965  poimirlem23  37968  poimirlem24  37969  poimirlem25  37970  poimirlem28  37973  poimirlem29  37974  poimirlem31  37976  itg2addnclem  37996  sticksstones11  42599  readvrec  42798  rabren3dioph  43251  2nn0ind  43381  flcidc  43606  dfrcl4  44111  fvilbdRP  44125  fvrcllb1d  44130  iunrelexp0  44137  corclrcl  44142  relexp1idm  44149  cotrcltrcl  44160  trclfvdecomr  44163  corcltrcl  44174  cotrclrcl  44177  dvsid  44766  binomcxplemnotnn0  44791  refsum2cnlem1  45476  infleinf  45809  itgsin0pilem1  46386  fourierdlem29  46572  fourierdlem56  46598  fourierdlem62  46604  fourierswlem  46666  fouriersw  46667  nthrucw  47322  lamberte  47338  cjnpoly  47339  fun2dmnopgexmpl  47734  sbgoldbo  48265  nnsum3primes4  48266  nnsum3primesgbe  48270  nnsum4primesodd  48274  nnsum4primesoddALTV  48275  cycl3grtrilem  48424  stgr1  48439  usgrexmpl1lem  48499  usgrexmpl1tri  48503  usgrexmpl2lem  48504  usgrexmpl2nb0  48509  usgrexmpl2nb1  48510  usgrexmpl2nb2  48511  usgrexmpl2trifr  48515  gpgiedgdmellem  48524  gpgvtx1  48532  opgpgvtx  48533  gpgedgvtx1  48540  gpgvtxedg0  48541  gpgvtxedg1  48542  gpgedgiov  48543  gpgedg2iv  48545  gpg5nbgrvtx03starlem1  48546  gpg5nbgrvtx03starlem3  48548  gpg5nbgrvtx13starlem1  48549  gpg5nbgrvtx13starlem2  48550  gpg5nbgrvtx13starlem3  48551  gpg3nbgrvtx0  48554  gpg3nbgrvtx0ALT  48555  gpg3nbgrvtx1  48556  gpgcubic  48557  gpg5nbgr3star  48559  gpg3kgrtriex  48567  gpgprismgr4cycllem2  48574  gpgprismgr4cycllem3  48575  gpgprismgr4cycllem7  48579  gpgprismgr4cycllem9  48581  pgnioedg1  48586  pgnioedg2  48587  pgnioedg3  48588  pgnioedg4  48589  pgnioedg5  48590  pgnbgreunbgrlem2lem1  48592  pgnbgreunbgrlem2lem2  48593  pgnbgreunbgrlem2lem3  48594  pgnbgreunbgrlem2  48595  pgnbgreunbgrlem3  48596  pgnbgreunbgrlem4  48597  pgnbgreunbgrlem5lem1  48598  pgnbgreunbgrlem5lem2  48599  pgnbgreunbgrlem5lem3  48600  pgnbgreunbgrlem6  48602  gpg5edgnedg  48608  grlimedgnedg  48609  zlmodzxzel  48833  zlmodzxz0  48834  zlmodzxzscm  48835  zlmodzxzadd  48836  blenval  49049  nn0sumshdiglemB  49098  fv2arycl  49126  2arympt  49127  2arymptfv  49128  2arymaptf1  49131  2arymaptfo  49132  fv1prop  49177  rrx2pxel  49189  prelrrx2  49191  prelrrx2b  49192  rrx2pnecoorneor  49193  rrx2xpref1o  49196  rrx2plordisom  49201  ehl2eudisval0  49203  rrx2line  49218  rrx2linest  49220  rrx2linesl  49221  2sphere0  49228  line2ylem  49229  line2  49230  line2xlem  49231  line2x  49232  line2y  49233  itscnhlinecirc02p  49263  inlinecirc02plem  49264