Theorem 1ex 11170

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ℂcc 11065  1c1 11068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-1cn 11125

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455

This theorem is referenced by:  1elpr01  11171  1nn  12215  dfnn2  12217  nn1suc  12226  1eltp012  12282  nn0ind-raph  12667  fzprval  13584  fztpval  13585  expval  14070  m1expcl2  14092  1exp  14098  facnn  14282  fac0  14283  prhash2ex  14406  funcnvs2  14920  funcnvs3  14921  funcnvs4  14922  wrdlen2i  14949  wrd2pr2op  14950  wrd3tpop  14955  wwlktovf1  14964  wrdl3s3  14969  relexp1g  15033  dfid6  15035  sgnval  15095  sgncl  15103  harmonic  15880  prodf1f  15913  fprodntriv  15963  prod1  15965  fprodss  15969  fprodn0f  16012  ege2le3  16111  ruclem8  16260  ruclem11  16263  1nprm  16704  pcmpt  16919  smndex2dnrinv  18943  mgmnsgrpex  18959  pmtrprfval  19518  pmtrprfvalrn  19519  psgnprfval  19552  psgnprfval1  19553  abvtrivd  20869  pzriprng1ALT  21536  cnmsgnsubg  21617  psdmplcl  22215  psdmul  22219  psdmvr  22222  m2detleiblem1  22672  m2detleiblem5  22673  m2detleiblem6  22674  m2detleiblem3  22677  m2detleiblem4  22678  m2detleib  22679  imasdsf1olem  24421  pcopt  25072  pcopt2  25073  pcoass  25074  ehl1eudis  25470  ehl2eudis  25472  voliunlem1  25600  i1f1lem  25739  i1f1  25740  itg11  25741  iblcnlem1  25838  bddibl  25890  dvexp  26003  dvef  26030  mvth  26042  iaa  26377  aalioulem2  26385  efrlim  27022  amgmlem  27042  amgm  27043  wilthlem2  27121  wilthlem3  27122  basellem7  27139  basellem9  27141  ppiublem2  27255  pclogsum  27267  bposlem5  27340  lgsfval  27354  lgsdir2lem3  27379  lgsdir  27384  lgsdilem2  27385  lgsdi  27386  lgsne0  27387  addsqnreup  27495  ostth1  27685  istrkg2ld  28617  axlowdimlem4  29103  axlowdimlem6  29105  axlowdimlem10  29109  axlowdimlem11  29110  axlowdimlem12  29111  axlowdimlem13  29112  axlowdim1  29117  umgr2v2eedg  29682  umgr2v2e  29683  umgr2v2evd2  29685  2wlklem  29823  usgr2trlncl  29917  2wlkdlem4  30085  2wlkdlem5  30086  2pthdlem1  30087  2wlkdlem10  30092  wwlks2onv  30110  elwwlks2ons3im  30111  usgrwwlks2on  30115  umgrwwlks2on  30116  3wlkdlem4  30321  3wlkdlem5  30322  3pthdlem1  30323  3wlkdlem10  30328  upgr3v3e3cycl  30339  upgr4cycl4dv4e  30344  konigsberglem4  30414  konigsberglem5  30415  ex-xp  30595  nmopun  32174  pjnmopi  32308  iuninc  32720  fprodex01  32988  s2rnOLD  33083  s3rnOLD  33085  psgnid  33238  cyc3fv2  33279  cnmsgn0g  33287  cyc3evpm  33291  sgnsval  33302  sgnsf  33303  1fldgenq  33470  gsumind  33492  esplyfvaln  33832  nn0constr  34019  cntnevol  34486  ddeval1  34492  ddeval0  34493  eulerpartgbij  34630  coinfliprv  34741  prodfzo03  34858  circlevma  34897  circlemethhgt  34898  hgt750lemg  34909  hgt750lemb  34911  hgt750lema  34912  tgoldbachgtde  34915  tgoldbachgt  34918  subfacp1lem1  35490  subfacp1lem2a  35491  subfacp1lem3  35493  subfacp1lem5  35495  cvmliftlem10  35605  sinccvglem  35983  poimirlem1  38081  poimirlem2  38082  poimirlem3  38083  poimirlem4  38084  poimirlem6  38086  poimirlem7  38087  poimirlem10  38090  poimirlem11  38091  poimirlem12  38092  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem28  38108  poimirlem29  38109  poimirlem31  38111  itg2addnclem  38131  sticksstones11  42734  readvrec  42932  rabren3dioph  43353  2nn0ind  43483  flcidc  43708  dfrcl4  44213  fvilbdRP  44227  fvrcllb1d  44232  iunrelexp0  44239  corclrcl  44244  relexp1idm  44251  cotrcltrcl  44262  trclfvdecomr  44265  corcltrcl  44276  cotrclrcl  44279  dvsid  44868  binomcxplemnotnn0  44893  refsum2cnlem1  45578  infleinf  45908  itgsin0pilem1  46485  fourierdlem29  46671  fourierdlem56  46697  fourierdlem62  46703  fourierswlem  46765  fouriersw  46766  nthrucw  47423  lamberte  47443  cjnpoly  47444  fun2dmnopgexmpl  47839  sbgoldbo  48370  nnsum3primes4  48371  nnsum3primesgbe  48375  nnsum4primesodd  48379  nnsum4primesoddALTV  48380  cycl3grtrilem  48529  stgr1  48544  usgrexmpl1lem  48604  usgrexmpl1tri  48608  usgrexmpl2lem  48609  usgrexmpl2nb0  48614  usgrexmpl2nb1  48615  usgrexmpl2nb2  48616  usgrexmpl2trifr  48620  gpgiedgdmellem  48629  gpgvtx1  48637  opgpgvtx  48638  gpgedgvtx1  48645  gpgvtxedg0  48646  gpgvtxedg1  48647  gpgedgiov  48648  gpgedg2iv  48650  gpg5nbgrvtx03starlem1  48651  gpg5nbgrvtx03starlem3  48653  gpg5nbgrvtx13starlem1  48654  gpg5nbgrvtx13starlem2  48655  gpg5nbgrvtx13starlem3  48656  gpg3nbgrvtx0  48659  gpg3nbgrvtx0ALT  48660  gpg3nbgrvtx1  48661  gpgcubic  48662  gpg5nbgr3star  48664  gpg3kgrtriex  48672  gpgprismgr4cycllem2  48679  gpgprismgr4cycllem3  48680  gpgprismgr4cycllem7  48684  gpgprismgr4cycllem9  48686  pgnioedg1  48691  pgnioedg2  48692  pgnioedg3  48693  pgnioedg4  48694  pgnioedg5  48695  pgnbgreunbgrlem2lem1  48697  pgnbgreunbgrlem2lem2  48698  pgnbgreunbgrlem2lem3  48699  pgnbgreunbgrlem2  48700  pgnbgreunbgrlem3  48701  pgnbgreunbgrlem4  48702  pgnbgreunbgrlem5lem1  48703  pgnbgreunbgrlem5lem2  48704  pgnbgreunbgrlem5lem3  48705  pgnbgreunbgrlem6  48707  gpg5edgnedg  48713  zlmodzxzel  48938  zlmodzxz0  48939  zlmodzxzscm  48940  zlmodzxzadd  48941  blenval  49154  nn0sumshdiglemB  49203  fv2arycl  49231  2arympt  49232  2arymptfv  49233  2arymaptf1  49236  2arymaptfo  49237  fv1prop  49282  rrx2pxel  49294  prelrrx2  49296  prelrrx2b  49297  rrx2pnecoorneor  49298  rrx2xpref1o  49301  rrx2plordisom  49306  ehl2eudisval0  49308  rrx2line  49323  rrx2linest  49325  rrx2linesl  49326  2sphere0  49333  line2ylem  49334  line2  49335  line2xlem  49336  line2x  49337  line2y  49338  itscnhlinecirc02p  49368  inlinecirc02plem  49369