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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ℂcc 11066  1c1 11069

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 11126

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 3449

This theorem is referenced by:  1nn  12197  dfnn2  12199  nn1suc  12208  nn0ind-raph  12634  fzprval  13546  fztpval  13547  expval  14028  m1expcl2  14050  1exp  14056  facnn  14240  fac0  14241  prhash2ex  14364  funcnvs2  14879  funcnvs3  14880  funcnvs4  14881  wrdlen2i  14908  wrd2pr2op  14909  wrd3tpop  14914  wwlktovf1  14923  wrdl3s3  14928  relexp1g  14992  dfid6  14994  sgnval  15054  harmonic  15825  prodf1f  15858  fprodntriv  15908  prod1  15910  fprodss  15914  fprodn0f  15957  ege2le3  16056  ruclem8  16205  ruclem11  16208  1nprm  16649  pcmpt  16863  smndex2dnrinv  18842  mgmnsgrpex  18858  pmtrprfval  19417  pmtrprfvalrn  19418  psgnprfval  19451  psgnprfval1  19452  abvtrivd  20741  pzriprng1ALT  21406  cnmsgnsubg  21486  psdmplcl  22049  psdmul  22053  psdmvr  22056  m2detleiblem1  22511  m2detleiblem5  22512  m2detleiblem6  22513  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  imasdsf1olem  24261  pcopt  24922  pcopt2  24923  pcoass  24924  ehl1eudis  25320  ehl2eudis  25322  voliunlem1  25451  i1f1lem  25590  i1f1  25591  itg11  25592  iblcnlem1  25689  bddibl  25741  dvexp  25857  dvef  25884  mvth  25897  iaa  26233  aalioulem2  26241  efrlim  26879  efrlimOLD  26880  amgmlem  26900  amgm  26901  wilthlem2  26979  wilthlem3  26980  basellem7  26997  basellem9  26999  ppiublem2  27114  pclogsum  27126  bposlem5  27199  lgsfval  27213  lgsdir2lem3  27238  lgsdir  27243  lgsdilem2  27244  lgsdi  27245  lgsne0  27246  addsqnreup  27354  ostth1  27544  istrkg2ld  28387  axlowdimlem4  28872  axlowdimlem6  28874  axlowdimlem10  28878  axlowdimlem11  28879  axlowdimlem12  28880  axlowdimlem13  28881  axlowdim1  28886  umgr2v2eedg  29452  umgr2v2e  29453  umgr2v2evd2  29455  2wlklem  29595  usgr2trlncl  29690  2wlkdlem4  29858  2wlkdlem5  29859  2pthdlem1  29860  2wlkdlem10  29865  wwlks2onv  29883  elwwlks2ons3im  29884  umgrwwlks2on  29887  3wlkdlem4  30091  3wlkdlem5  30092  3pthdlem1  30093  3wlkdlem10  30098  upgr3v3e3cycl  30109  upgr4cycl4dv4e  30114  konigsberglem4  30184  konigsberglem5  30185  ex-xp  30365  nmopun  31943  pjnmopi  32077  iuninc  32489  fprodex01  32750  sgncl  32756  s2rnOLD  32865  s3rnOLD  32867  psgnid  33054  cyc3fv2  33095  cnmsgn0g  33103  cyc3evpm  33107  sgnsval  33118  sgnsf  33119  1fldgenq  33272  constrconj  33735  nn0constr  33751  cntnevol  34218  ddeval1  34224  ddeval0  34225  eulerpartgbij  34363  coinfliprv  34474  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  subfacp1lem1  35166  subfacp1lem2a  35167  subfacp1lem3  35169  subfacp1lem5  35171  cvmliftlem10  35281  sinccvglem  35659  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  itg2addnclem  37665  sticksstones11  42144  readvrec  42350  rabren3dioph  42803  2nn0ind  42934  flcidc  43159  dfrcl4  43665  fvilbdRP  43679  fvrcllb1d  43684  iunrelexp0  43691  corclrcl  43696  relexp1idm  43703  cotrcltrcl  43714  trclfvdecomr  43717  corcltrcl  43728  cotrclrcl  43731  dvsid  44320  binomcxplemnotnn0  44345  refsum2cnlem1  45031  infleinf  45368  itgsin0pilem1  45948  fourierdlem29  46134  fourierdlem56  46160  fourierdlem62  46166  fourierswlem  46228  fouriersw  46229  lamberte  46889  cjnpoly  46890  fun2dmnopgexmpl  47285  sbgoldbo  47788  nnsum3primes4  47789  nnsum3primesgbe  47793  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  cycl3grtrilem  47945  stgr1  47960  usgrexmpl1lem  48012  usgrexmpl1tri  48016  usgrexmpl2lem  48017  usgrexmpl2nb0  48022  usgrexmpl2nb1  48023  usgrexmpl2nb2  48024  usgrexmpl2trifr  48028  gpgiedgdmellem  48037  gpgvtx1  48045  opgpgvtx  48046  gpgedgvtx1  48053  gpgvtxedg0  48054  gpgvtxedg1  48055  gpgedgiov  48056  gpgedg2iv  48058  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpgcubic  48070  gpg5nbgr3star  48072  gpg3kgrtriex  48080  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem3  48087  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem9  48093  pgnioedg1  48098  pgnioedg2  48099  pgnioedg3  48100  pgnioedg4  48101  pgnioedg5  48102  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  pgnbgreunbgrlem2  48107  pgnbgreunbgrlem3  48108  pgnbgreunbgrlem4  48109  pgnbgreunbgrlem5lem1  48110  pgnbgreunbgrlem5lem2  48111  pgnbgreunbgrlem5lem3  48112  pgnbgreunbgrlem6  48114  zlmodzxzel  48343  zlmodzxz0  48344  zlmodzxzscm  48345  zlmodzxzadd  48346  blenval  48560  nn0sumshdiglemB  48609  fv2arycl  48637  2arympt  48638  2arymptfv  48639  2arymaptf1  48642  2arymaptfo  48643  fv1prop  48688  rrx2pxel  48700  prelrrx2  48702  prelrrx2b  48703  rrx2pnecoorneor  48704  rrx2xpref1o  48707  rrx2plordisom  48712  ehl2eudisval0  48714  rrx2line  48729  rrx2linest  48731  rrx2linesl  48732  2sphere0  48739  line2ylem  48740  line2  48741  line2xlem  48742  line2x  48743  line2y  48744  itscnhlinecirc02p  48774  inlinecirc02plem  48775