Theorem 1ex 10902

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ℂcc 10800  1c1 10803

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-1cn 10860

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424

This theorem is referenced by:  1nn  11914  dfnn2  11916  nn1suc  11925  nn0ind-raph  12350  fzprval  13246  fztpval  13247  expval  13712  m1expcl2  13732  1exp  13740  facnn  13917  fac0  13918  prhash2ex  14042  funcnvs2  14554  funcnvs3  14555  funcnvs4  14556  wrdlen2i  14583  wrd2pr2op  14584  wrd3tpop  14589  wwlktovf1  14600  wrdl3s3  14605  relexp1g  14665  dfid6  14667  sgnval  14727  harmonic  15499  prodf1f  15532  fprodntriv  15580  prod1  15582  fprodss  15586  fprodn0f  15629  ege2le3  15727  ruclem8  15874  ruclem11  15877  1nprm  16312  pcmpt  16521  smndex2dnrinv  18469  mgmnsgrpex  18485  pmtrprfval  19010  pmtrprfvalrn  19011  psgnprfval  19044  psgnprfval1  19045  abvtrivd  20015  cnmsgnsubg  20694  m2detleiblem1  21681  m2detleiblem5  21682  m2detleiblem6  21683  m2detleiblem3  21686  m2detleiblem4  21687  m2detleib  21688  imasdsf1olem  23434  pcopt  24091  pcopt2  24092  pcoass  24093  ehl1eudis  24489  ehl2eudis  24491  voliunlem1  24619  i1f1lem  24758  i1f1  24759  itg11  24760  iblcnlem1  24857  bddibl  24909  dvexp  25022  dvef  25049  mvth  25061  iaa  25390  aalioulem2  25398  efrlim  26024  amgmlem  26044  amgm  26045  wilthlem2  26123  wilthlem3  26124  basellem7  26141  basellem9  26143  ppiublem2  26256  pclogsum  26268  bposlem5  26341  lgsfval  26355  lgsdir2lem3  26380  lgsdir  26385  lgsdilem2  26386  lgsdi  26387  lgsne0  26388  addsqnreup  26496  ostth1  26686  istrkg2ld  26725  axlowdimlem4  27216  axlowdimlem6  27218  axlowdimlem10  27222  axlowdimlem11  27223  axlowdimlem12  27224  axlowdimlem13  27225  axlowdim1  27230  umgr2v2eedg  27794  umgr2v2e  27795  umgr2v2evd2  27797  2wlklem  27937  usgr2trlncl  28029  2wlkdlem4  28194  2wlkdlem5  28195  2pthdlem1  28196  2wlkdlem10  28201  wwlks2onv  28219  elwwlks2ons3im  28220  umgrwwlks2on  28223  3wlkdlem4  28427  3wlkdlem5  28428  3pthdlem1  28429  3wlkdlem10  28434  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  konigsberglem4  28520  konigsberglem5  28521  ex-xp  28701  nmopun  30277  pjnmopi  30411  iuninc  30801  fprodex01  31041  s2rn  31120  s3rn  31122  psgnid  31266  cyc3fv2  31307  cnmsgn0g  31315  cyc3evpm  31319  sgnsval  31330  sgnsf  31331  cntnevol  32096  ddeval1  32102  ddeval0  32103  eulerpartgbij  32239  coinfliprv  32349  sgncl  32405  prodfzo03  32483  circlevma  32522  circlemethhgt  32523  hgt750lemg  32534  hgt750lemb  32536  hgt750lema  32537  hgt750leme  32538  tgoldbachgtde  32540  tgoldbachgt  32543  subfacp1lem1  33041  subfacp1lem2a  33042  subfacp1lem3  33044  subfacp1lem5  33046  cvmliftlem10  33156  sinccvglem  33530  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  itg2addnclem  35755  sticksstones11  40040  rabren3dioph  40553  2nn0ind  40683  flcidc  40915  dfrcl4  41173  fvilbdRP  41187  fvrcllb1d  41192  iunrelexp0  41199  corclrcl  41204  relexp1idm  41211  cotrcltrcl  41222  trclfvdecomr  41225  corcltrcl  41236  cotrclrcl  41239  dvsid  41838  binomcxplemnotnn0  41863  refsum2cnlem1  42469  infleinf  42801  itgsin0pilem1  43381  fourierdlem29  43567  fourierdlem56  43593  fourierdlem62  43599  fourierswlem  43661  fouriersw  43662  fun2dmnopgexmpl  44663  sbgoldbo  45127  nnsum3primes4  45128  nnsum3primesgbe  45132  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  zlmodzxzel  45579  zlmodzxz0  45580  zlmodzxzscm  45581  zlmodzxzadd  45582  blenval  45805  nn0sumshdiglemB  45854  fv2arycl  45882  2arympt  45883  2arymptfv  45884  2arymaptf1  45887  2arymaptfo  45888  fv1prop  45933  rrx2pxel  45945  prelrrx2  45947  prelrrx2b  45948  rrx2pnecoorneor  45949  rrx2xpref1o  45952  rrx2plordisom  45957  ehl2eudisval0  45959  rrx2line  45974  rrx2linest  45976  rrx2linesl  45977  2sphere0  45984  line2ylem  45985  line2  45986  line2xlem  45987  line2x  45988  line2y  45989  itscnhlinecirc02p  46019  inlinecirc02plem  46020