Theorem 1ex 10972

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

Syntax hints:   ∈ wcel 2110  Vcvv 3431  ℂcc 10870  1c1 10873

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-1cn 10930

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433

This theorem is referenced by:  1nn  11984  dfnn2  11986  nn1suc  11995  nn0ind-raph  12420  fzprval  13316  fztpval  13317  expval  13782  m1expcl2  13802  1exp  13810  facnn  13987  fac0  13988  prhash2ex  14112  funcnvs2  14624  funcnvs3  14625  funcnvs4  14626  wrdlen2i  14653  wrd2pr2op  14654  wrd3tpop  14659  wwlktovf1  14670  wrdl3s3  14675  relexp1g  14735  dfid6  14737  sgnval  14797  harmonic  15569  prodf1f  15602  fprodntriv  15650  prod1  15652  fprodss  15656  fprodn0f  15699  ege2le3  15797  ruclem8  15944  ruclem11  15947  1nprm  16382  pcmpt  16591  smndex2dnrinv  18552  mgmnsgrpex  18568  pmtrprfval  19093  pmtrprfvalrn  19094  psgnprfval  19127  psgnprfval1  19128  abvtrivd  20098  cnmsgnsubg  20780  m2detleiblem1  21771  m2detleiblem5  21772  m2detleiblem6  21773  m2detleiblem3  21776  m2detleiblem4  21777  m2detleib  21778  imasdsf1olem  23524  pcopt  24183  pcopt2  24184  pcoass  24185  ehl1eudis  24582  ehl2eudis  24584  voliunlem1  24712  i1f1lem  24851  i1f1  24852  itg11  24853  iblcnlem1  24950  bddibl  25002  dvexp  25115  dvef  25142  mvth  25154  iaa  25483  aalioulem2  25491  efrlim  26117  amgmlem  26137  amgm  26138  wilthlem2  26216  wilthlem3  26217  basellem7  26234  basellem9  26236  ppiublem2  26349  pclogsum  26361  bposlem5  26434  lgsfval  26448  lgsdir2lem3  26473  lgsdir  26478  lgsdilem2  26479  lgsdi  26480  lgsne0  26481  addsqnreup  26589  ostth1  26779  istrkg2ld  26819  axlowdimlem4  27311  axlowdimlem6  27313  axlowdimlem10  27317  axlowdimlem11  27318  axlowdimlem12  27319  axlowdimlem13  27320  axlowdim1  27325  umgr2v2eedg  27889  umgr2v2e  27890  umgr2v2evd2  27892  2wlklem  28032  usgr2trlncl  28124  2wlkdlem4  28289  2wlkdlem5  28290  2pthdlem1  28291  2wlkdlem10  28296  wwlks2onv  28314  elwwlks2ons3im  28315  umgrwwlks2on  28318  3wlkdlem4  28522  3wlkdlem5  28523  3pthdlem1  28524  3wlkdlem10  28529  upgr3v3e3cycl  28540  upgr4cycl4dv4e  28545  konigsberglem4  28615  konigsberglem5  28616  ex-xp  28796  nmopun  30372  pjnmopi  30506  iuninc  30896  fprodex01  31135  s2rn  31214  s3rn  31216  psgnid  31360  cyc3fv2  31401  cnmsgn0g  31409  cyc3evpm  31413  sgnsval  31424  sgnsf  31425  cntnevol  32192  ddeval1  32198  ddeval0  32199  eulerpartgbij  32335  coinfliprv  32445  sgncl  32501  prodfzo03  32579  circlevma  32618  circlemethhgt  32619  hgt750lemg  32630  hgt750lemb  32632  hgt750lema  32633  hgt750leme  32634  tgoldbachgtde  32636  tgoldbachgt  32639  subfacp1lem1  33137  subfacp1lem2a  33138  subfacp1lem3  33140  subfacp1lem5  33142  cvmliftlem10  33252  sinccvglem  33626  poimirlem1  35774  poimirlem2  35775  poimirlem3  35776  poimirlem4  35777  poimirlem6  35779  poimirlem7  35780  poimirlem10  35783  poimirlem11  35784  poimirlem12  35785  poimirlem16  35789  poimirlem17  35790  poimirlem19  35792  poimirlem20  35793  poimirlem23  35796  poimirlem24  35797  poimirlem25  35798  poimirlem28  35801  poimirlem29  35802  poimirlem31  35804  itg2addnclem  35824  sticksstones11  40109  rabren3dioph  40634  2nn0ind  40764  flcidc  40996  dfrcl4  41254  fvilbdRP  41268  fvrcllb1d  41273  iunrelexp0  41280  corclrcl  41285  relexp1idm  41292  cotrcltrcl  41303  trclfvdecomr  41306  corcltrcl  41317  cotrclrcl  41320  dvsid  41919  binomcxplemnotnn0  41944  refsum2cnlem1  42550  infleinf  42882  itgsin0pilem1  43462  fourierdlem29  43648  fourierdlem56  43674  fourierdlem62  43680  fourierswlem  43742  fouriersw  43743  fun2dmnopgexmpl  44744  sbgoldbo  45208  nnsum3primes4  45209  nnsum3primesgbe  45213  nnsum4primesodd  45217  nnsum4primesoddALTV  45218  zlmodzxzel  45660  zlmodzxz0  45661  zlmodzxzscm  45662  zlmodzxzadd  45663  blenval  45886  nn0sumshdiglemB  45935  fv2arycl  45963  2arympt  45964  2arymptfv  45965  2arymaptf1  45968  2arymaptfo  45969  fv1prop  46014  rrx2pxel  46026  prelrrx2  46028  prelrrx2b  46029  rrx2pnecoorneor  46030  rrx2xpref1o  46033  rrx2plordisom  46038  ehl2eudisval0  46040  rrx2line  46055  rrx2linest  46057  rrx2linesl  46058  2sphere0  46065  line2ylem  46066  line2  46067  line2xlem  46068  line2x  46069  line2y  46070  itscnhlinecirc02p  46100  inlinecirc02plem  46101