Theorem 1ex 11206

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ℂcc 11104  1c1 11107

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-1cn 11164

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476

This theorem is referenced by:  1nn  12219  dfnn2  12221  nn1suc  12230  nn0ind-raph  12658  fzprval  13558  fztpval  13559  expval  14025  m1expcl2  14047  1exp  14053  facnn  14231  fac0  14232  prhash2ex  14355  funcnvs2  14860  funcnvs3  14861  funcnvs4  14862  wrdlen2i  14889  wrd2pr2op  14890  wrd3tpop  14895  wwlktovf1  14904  wrdl3s3  14909  relexp1g  14969  dfid6  14971  sgnval  15031  harmonic  15801  prodf1f  15834  fprodntriv  15882  prod1  15884  fprodss  15888  fprodn0f  15931  ege2le3  16029  ruclem8  16176  ruclem11  16179  1nprm  16612  pcmpt  16821  smndex2dnrinv  18792  mgmnsgrpex  18808  pmtrprfval  19349  pmtrprfvalrn  19350  psgnprfval  19383  psgnprfval1  19384  abvtrivd  20440  cnmsgnsubg  21121  m2detleiblem1  22117  m2detleiblem5  22118  m2detleiblem6  22119  m2detleiblem3  22122  m2detleiblem4  22123  m2detleib  22124  imasdsf1olem  23870  pcopt  24529  pcopt2  24530  pcoass  24531  ehl1eudis  24928  ehl2eudis  24930  voliunlem1  25058  i1f1lem  25197  i1f1  25198  itg11  25199  iblcnlem1  25296  bddibl  25348  dvexp  25461  dvef  25488  mvth  25500  iaa  25829  aalioulem2  25837  efrlim  26463  amgmlem  26483  amgm  26484  wilthlem2  26562  wilthlem3  26563  basellem7  26580  basellem9  26582  ppiublem2  26695  pclogsum  26707  bposlem5  26780  lgsfval  26794  lgsdir2lem3  26819  lgsdir  26824  lgsdilem2  26825  lgsdi  26826  lgsne0  26827  addsqnreup  26935  ostth1  27125  istrkg2ld  27700  axlowdimlem4  28192  axlowdimlem6  28194  axlowdimlem10  28198  axlowdimlem11  28199  axlowdimlem12  28200  axlowdimlem13  28201  axlowdim1  28206  umgr2v2eedg  28770  umgr2v2e  28771  umgr2v2evd2  28773  2wlklem  28913  usgr2trlncl  29006  2wlkdlem4  29171  2wlkdlem5  29172  2pthdlem1  29173  2wlkdlem10  29178  wwlks2onv  29196  elwwlks2ons3im  29197  umgrwwlks2on  29200  3wlkdlem4  29404  3wlkdlem5  29405  3pthdlem1  29406  3wlkdlem10  29411  upgr3v3e3cycl  29422  upgr4cycl4dv4e  29427  konigsberglem4  29497  konigsberglem5  29498  ex-xp  29678  nmopun  31254  pjnmopi  31388  iuninc  31779  fprodex01  32018  s2rn  32097  s3rn  32099  psgnid  32243  cyc3fv2  32284  cnmsgn0g  32292  cyc3evpm  32296  sgnsval  32307  sgnsf  32308  1fldgenq  32400  cntnevol  33214  ddeval1  33220  ddeval0  33221  eulerpartgbij  33359  coinfliprv  33469  sgncl  33525  prodfzo03  33603  circlevma  33642  circlemethhgt  33643  hgt750lemg  33654  hgt750lemb  33656  hgt750lema  33657  hgt750leme  33658  tgoldbachgtde  33660  tgoldbachgt  33663  subfacp1lem1  34158  subfacp1lem2a  34159  subfacp1lem3  34161  subfacp1lem5  34163  cvmliftlem10  34273  sinccvglem  34645  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem6  36482  poimirlem7  36483  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem28  36504  poimirlem29  36505  poimirlem31  36507  itg2addnclem  36527  sticksstones11  40960  rabren3dioph  41538  2nn0ind  41669  flcidc  41901  dfrcl4  42412  fvilbdRP  42426  fvrcllb1d  42431  iunrelexp0  42438  corclrcl  42443  relexp1idm  42450  cotrcltrcl  42461  trclfvdecomr  42464  corcltrcl  42475  cotrclrcl  42478  dvsid  43075  binomcxplemnotnn0  43100  refsum2cnlem1  43706  infleinf  44068  itgsin0pilem1  44652  fourierdlem29  44838  fourierdlem56  44864  fourierdlem62  44870  fourierswlem  44932  fouriersw  44933  fun2dmnopgexmpl  45978  sbgoldbo  46441  nnsum3primes4  46442  nnsum3primesgbe  46446  nnsum4primesodd  46450  nnsum4primesoddALTV  46451  zlmodzxzel  46984  zlmodzxz0  46985  zlmodzxzscm  46986  zlmodzxzadd  46987  blenval  47210  nn0sumshdiglemB  47259  fv2arycl  47287  2arympt  47288  2arymptfv  47289  2arymaptf1  47292  2arymaptfo  47293  fv1prop  47338  rrx2pxel  47350  prelrrx2  47352  prelrrx2b  47353  rrx2pnecoorneor  47354  rrx2xpref1o  47357  rrx2plordisom  47362  ehl2eudisval0  47364  rrx2line  47379  rrx2linest  47381  rrx2linesl  47382  2sphere0  47389  line2ylem  47390  line2  47391  line2xlem  47392  line2x  47393  line2y  47394  itscnhlinecirc02p  47424  inlinecirc02plem  47425