Theorem 1ex 10427

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

Syntax hints:   ∈ wcel 2048  Vcvv 3409  ℂcc 10325  1c1 10328

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-ext 2745  ax-1cn 10385

This theorem depends on definitions:  df-bi 199  df-an 388  df-ex 1743  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-v 3411

This theorem is referenced by:  1nn  11444  dfnn2  11446  nn1suc  11454  nn0ind-raph  11888  fzprval  12777  fztpval  12778  expval  13239  m1expcl2  13259  1exp  13266  facnn  13443  fac0  13444  prhash2ex  13564  funcnvs2  14127  funcnvs3  14128  funcnvs4  14129  wrdlen2i  14156  wrd2pr2op  14157  wrd3tpop  14162  wwlktovf1  14172  wrdl3s3  14177  relexp1g  14236  dfid6  14238  sgnval  14298  harmonic  15064  prodf1f  15098  fprodntriv  15146  prod1  15148  fprodss  15152  fprodn0f  15195  ege2le3  15293  ruclem8  15440  ruclem11  15443  1nprm  15869  pcmpt  16074  mgmnsgrpex  17877  pmtrprfval  18366  pmtrprfvalrn  18367  psgnprfval  18401  psgnprfval1  18402  abvtrivd  19323  cnmsgnsubg  20413  m2detleiblem1  20927  m2detleiblem5  20928  m2detleiblem6  20929  m2detleiblem3  20932  m2detleiblem4  20933  m2detleib  20934  imasdsf1olem  22676  pcopt  23319  pcopt2  23320  pcoass  23321  ehl1eudis  23716  ehl2eudis  23718  voliunlem1  23844  i1f1lem  23983  i1f1  23984  itg11  23985  iblcnlem1  24081  bddibl  24133  dvexp  24243  dvef  24270  mvth  24282  iaa  24607  aalioulem2  24615  efrlim  25239  amgmlem  25259  amgm  25260  wilthlem2  25338  wilthlem3  25339  basellem7  25356  basellem9  25358  ppiublem2  25471  pclogsum  25483  bposlem5  25556  lgsfval  25570  lgsdir2lem3  25595  lgsdir  25600  lgsdilem2  25601  lgsdi  25602  lgsne0  25603  addsqnreup  25711  ostth1  25901  istrkg2ld  25938  axlowdimlem4  26424  axlowdimlem6  26426  axlowdimlem10  26430  axlowdimlem11  26431  axlowdimlem12  26432  axlowdimlem13  26433  axlowdim1  26438  umgr2v2eedg  26999  umgr2v2e  27000  umgr2v2evd2  27002  2wlklem  27141  usgr2trlncl  27239  2wlkdlem4  27424  2wlkdlem5  27425  2pthdlem1  27426  2wlkdlem10  27431  wwlks2onv  27449  elwwlks2ons3im  27450  umgrwwlks2on  27453  3wlkdlem4  27681  3wlkdlem5  27682  3pthdlem1  27683  3wlkdlem10  27688  upgr3v3e3cycl  27699  upgr4cycl4dv4e  27704  konigsberglem4  27777  konigsberglem5  27778  ex-xp  27983  nmopun  29562  pjnmopi  29696  iuninc  30071  fprodex01  30276  sgnsval  30425  sgnsf  30426  psgnid  30645  cntnevol  31089  ddeval1  31095  ddeval0  31096  eulerpartgbij  31232  coinfliprv  31343  sgncl  31399  prodfzo03  31483  circlevma  31522  circlemethhgt  31523  hgt750lemg  31534  hgt750lemb  31536  hgt750lema  31537  hgt750leme  31538  tgoldbachgtde  31540  tgoldbachgt  31543  subfacp1lem1  31971  subfacp1lem2a  31972  subfacp1lem3  31974  subfacp1lem5  31976  cvmliftlem10  32086  sinccvglem  32375  poimirlem1  34282  poimirlem2  34283  poimirlem3  34284  poimirlem4  34285  poimirlem6  34287  poimirlem7  34288  poimirlem10  34291  poimirlem11  34292  poimirlem12  34293  poimirlem16  34297  poimirlem17  34298  poimirlem19  34300  poimirlem20  34301  poimirlem23  34304  poimirlem24  34305  poimirlem25  34306  poimirlem28  34309  poimirlem29  34310  poimirlem31  34312  itg2addnclem  34332  rabren3dioph  38753  2nn0ind  38883  flcidc  39115  dfrcl4  39329  fvilbdRP  39343  fvrcllb1d  39348  iunrelexp0  39355  corclrcl  39360  relexp1idm  39367  cotrcltrcl  39378  trclfvdecomr  39381  corcltrcl  39392  cotrclrcl  39395  dvsid  40023  binomcxplemnotnn0  40048  refsum2cnlem1  40657  infleinf  41015  itgsin0pilem1  41611  fourierdlem29  41798  fourierdlem56  41824  fourierdlem62  41830  fourierswlem  41892  fouriersw  41893  fun2dmnopgexmpl  42835  sbgoldbo  43260  nnsum3primes4  43261  nnsum3primesgbe  43265  nnsum4primesodd  43269  nnsum4primesoddALTV  43270  zlmodzxzel  43707  zlmodzxz0  43708  zlmodzxzscm  43709  zlmodzxzadd  43710  blenval  43939  nn0sumshdiglemB  43988  fv1prop  43994  rrx2pxel  44006  prelrrx2  44008  prelrrx2b  44009  rrx2pnecoorneor  44010  rrx2xpref1o  44013  rrx2plordisom  44018  ehl2eudisval0  44020  rrx2line  44035  rrx2linest  44037  rrx2linesl  44038  2sphere0  44045  line2ylem  44046  line2  44047  line2xlem  44048  line2x  44049  line2y  44050  itscnhlinecirc02p  44080  inlinecirc02plem  44081