Theorem 1ex 10639

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  ℂcc 10537  1c1 10540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795  ax-1cn 10597

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-v 3498

This theorem is referenced by:  1nn  11651  dfnn2  11653  nn1suc  11662  nn0ind-raph  12085  fzprval  12971  fztpval  12972  expval  13434  m1expcl2  13454  1exp  13461  facnn  13638  fac0  13639  prhash2ex  13763  funcnvs2  14277  funcnvs3  14278  funcnvs4  14279  wrdlen2i  14306  wrd2pr2op  14307  wrd3tpop  14312  wwlktovf1  14323  wrdl3s3  14328  relexp1g  14387  dfid6  14389  sgnval  14449  harmonic  15216  prodf1f  15250  fprodntriv  15298  prod1  15300  fprodss  15304  fprodn0f  15347  ege2le3  15445  ruclem8  15592  ruclem11  15595  1nprm  16025  pcmpt  16230  smndex2dnrinv  18082  mgmnsgrpex  18098  pmtrprfval  18617  pmtrprfvalrn  18618  psgnprfval  18651  psgnprfval1  18652  abvtrivd  19613  cnmsgnsubg  20723  m2detleiblem1  21235  m2detleiblem5  21236  m2detleiblem6  21237  m2detleiblem3  21240  m2detleiblem4  21241  m2detleib  21242  imasdsf1olem  22985  pcopt  23628  pcopt2  23629  pcoass  23630  ehl1eudis  24025  ehl2eudis  24027  voliunlem1  24153  i1f1lem  24292  i1f1  24293  itg11  24294  iblcnlem1  24390  bddibl  24442  dvexp  24552  dvef  24579  mvth  24591  iaa  24916  aalioulem2  24924  efrlim  25549  amgmlem  25569  amgm  25570  wilthlem2  25648  wilthlem3  25649  basellem7  25666  basellem9  25668  ppiublem2  25781  pclogsum  25793  bposlem5  25866  lgsfval  25880  lgsdir2lem3  25905  lgsdir  25910  lgsdilem2  25911  lgsdi  25912  lgsne0  25913  addsqnreup  26021  ostth1  26211  istrkg2ld  26248  axlowdimlem4  26733  axlowdimlem6  26735  axlowdimlem10  26739  axlowdimlem11  26740  axlowdimlem12  26741  axlowdimlem13  26742  axlowdim1  26747  umgr2v2eedg  27308  umgr2v2e  27309  umgr2v2evd2  27311  2wlklem  27451  usgr2trlncl  27543  2wlkdlem4  27709  2wlkdlem5  27710  2pthdlem1  27711  2wlkdlem10  27716  wwlks2onv  27734  elwwlks2ons3im  27735  umgrwwlks2on  27738  3wlkdlem4  27943  3wlkdlem5  27944  3pthdlem1  27945  3wlkdlem10  27950  upgr3v3e3cycl  27961  upgr4cycl4dv4e  27966  konigsberglem4  28036  konigsberglem5  28037  ex-xp  28217  nmopun  29793  pjnmopi  29927  iuninc  30314  fprodex01  30543  s2rn  30622  s3rn  30624  psgnid  30741  cyc3fv2  30782  cnmsgn0g  30790  cyc3evpm  30794  sgnsval  30805  sgnsf  30806  cntnevol  31489  ddeval1  31495  ddeval0  31496  eulerpartgbij  31632  coinfliprv  31742  sgncl  31798  prodfzo03  31876  circlevma  31915  circlemethhgt  31916  hgt750lemg  31927  hgt750lemb  31929  hgt750lema  31930  hgt750leme  31931  tgoldbachgtde  31933  tgoldbachgt  31936  subfacp1lem1  32428  subfacp1lem2a  32429  subfacp1lem3  32431  subfacp1lem5  32433  cvmliftlem10  32543  sinccvglem  32917  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem6  34900  poimirlem7  34901  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem28  34922  poimirlem29  34923  poimirlem31  34925  itg2addnclem  34945  rabren3dioph  39419  2nn0ind  39549  flcidc  39781  dfrcl4  40028  fvilbdRP  40042  fvrcllb1d  40047  iunrelexp0  40054  corclrcl  40059  relexp1idm  40066  cotrcltrcl  40077  trclfvdecomr  40080  corcltrcl  40091  cotrclrcl  40094  dvsid  40670  binomcxplemnotnn0  40695  refsum2cnlem1  41301  infleinf  41647  itgsin0pilem1  42242  fourierdlem29  42428  fourierdlem56  42454  fourierdlem62  42460  fourierswlem  42522  fouriersw  42523  fun2dmnopgexmpl  43490  sbgoldbo  43959  nnsum3primes4  43960  nnsum3primesgbe  43964  nnsum4primesodd  43968  nnsum4primesoddALTV  43969  zlmodzxzel  44410  zlmodzxz0  44411  zlmodzxzscm  44412  zlmodzxzadd  44413  blenval  44638  nn0sumshdiglemB  44687  fv1prop  44693  rrx2pxel  44705  prelrrx2  44707  prelrrx2b  44708  rrx2pnecoorneor  44709  rrx2xpref1o  44712  rrx2plordisom  44717  ehl2eudisval0  44719  rrx2line  44734  rrx2linest  44736  rrx2linesl  44737  2sphere0  44744  line2ylem  44745  line2  44746  line2xlem  44747  line2x  44748  line2y  44749  itscnhlinecirc02p  44779  inlinecirc02plem  44780