Theorem 1ex 11210

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  ℂcc 11108  1c1 11111

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-1cn 11168

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477

This theorem is referenced by:  1nn  12223  dfnn2  12225  nn1suc  12234  nn0ind-raph  12662  fzprval  13562  fztpval  13563  expval  14029  m1expcl2  14051  1exp  14057  facnn  14235  fac0  14236  prhash2ex  14359  funcnvs2  14864  funcnvs3  14865  funcnvs4  14866  wrdlen2i  14893  wrd2pr2op  14894  wrd3tpop  14899  wwlktovf1  14908  wrdl3s3  14913  relexp1g  14973  dfid6  14975  sgnval  15035  harmonic  15805  prodf1f  15838  fprodntriv  15886  prod1  15888  fprodss  15892  fprodn0f  15935  ege2le3  16033  ruclem8  16180  ruclem11  16183  1nprm  16616  pcmpt  16825  smndex2dnrinv  18796  mgmnsgrpex  18812  pmtrprfval  19355  pmtrprfvalrn  19356  psgnprfval  19389  psgnprfval1  19390  abvtrivd  20448  cnmsgnsubg  21130  m2detleiblem1  22126  m2detleiblem5  22127  m2detleiblem6  22128  m2detleiblem3  22131  m2detleiblem4  22132  m2detleib  22133  imasdsf1olem  23879  pcopt  24538  pcopt2  24539  pcoass  24540  ehl1eudis  24937  ehl2eudis  24939  voliunlem1  25067  i1f1lem  25206  i1f1  25207  itg11  25208  iblcnlem1  25305  bddibl  25357  dvexp  25470  dvef  25497  mvth  25509  iaa  25838  aalioulem2  25846  efrlim  26474  amgmlem  26494  amgm  26495  wilthlem2  26573  wilthlem3  26574  basellem7  26591  basellem9  26593  ppiublem2  26706  pclogsum  26718  bposlem5  26791  lgsfval  26805  lgsdir2lem3  26830  lgsdir  26835  lgsdilem2  26836  lgsdi  26837  lgsne0  26838  addsqnreup  26946  ostth1  27136  istrkg2ld  27711  axlowdimlem4  28203  axlowdimlem6  28205  axlowdimlem10  28209  axlowdimlem11  28210  axlowdimlem12  28211  axlowdimlem13  28212  axlowdim1  28217  umgr2v2eedg  28781  umgr2v2e  28782  umgr2v2evd2  28784  2wlklem  28924  usgr2trlncl  29017  2wlkdlem4  29182  2wlkdlem5  29183  2pthdlem1  29184  2wlkdlem10  29189  wwlks2onv  29207  elwwlks2ons3im  29208  umgrwwlks2on  29211  3wlkdlem4  29415  3wlkdlem5  29416  3pthdlem1  29417  3wlkdlem10  29422  upgr3v3e3cycl  29433  upgr4cycl4dv4e  29438  konigsberglem4  29508  konigsberglem5  29509  ex-xp  29689  nmopun  31267  pjnmopi  31401  iuninc  31792  fprodex01  32031  s2rn  32110  s3rn  32112  psgnid  32256  cyc3fv2  32297  cnmsgn0g  32305  cyc3evpm  32309  sgnsval  32320  sgnsf  32321  1fldgenq  32412  cntnevol  33226  ddeval1  33232  ddeval0  33233  eulerpartgbij  33371  coinfliprv  33481  sgncl  33537  prodfzo03  33615  circlevma  33654  circlemethhgt  33655  hgt750lemg  33666  hgt750lemb  33668  hgt750lema  33669  hgt750leme  33670  tgoldbachgtde  33672  tgoldbachgt  33675  subfacp1lem1  34170  subfacp1lem2a  34171  subfacp1lem3  34173  subfacp1lem5  34175  cvmliftlem10  34285  sinccvglem  34657  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  itg2addnclem  36539  sticksstones11  40972  rabren3dioph  41553  2nn0ind  41684  flcidc  41916  dfrcl4  42427  fvilbdRP  42441  fvrcllb1d  42446  iunrelexp0  42453  corclrcl  42458  relexp1idm  42465  cotrcltrcl  42476  trclfvdecomr  42479  corcltrcl  42490  cotrclrcl  42493  dvsid  43090  binomcxplemnotnn0  43115  refsum2cnlem1  43721  infleinf  44082  itgsin0pilem1  44666  fourierdlem29  44852  fourierdlem56  44878  fourierdlem62  44884  fourierswlem  44946  fouriersw  44947  fun2dmnopgexmpl  45992  sbgoldbo  46455  nnsum3primes4  46456  nnsum3primesgbe  46460  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  pzriprng1ALT  46820  zlmodzxzel  47031  zlmodzxz0  47032  zlmodzxzscm  47033  zlmodzxzadd  47034  blenval  47257  nn0sumshdiglemB  47306  fv2arycl  47334  2arympt  47335  2arymptfv  47336  2arymaptf1  47339  2arymaptfo  47340  fv1prop  47385  rrx2pxel  47397  prelrrx2  47399  prelrrx2b  47400  rrx2pnecoorneor  47401  rrx2xpref1o  47404  rrx2plordisom  47409  ehl2eudisval0  47411  rrx2line  47426  rrx2linest  47428  rrx2linesl  47429  2sphere0  47436  line2ylem  47437  line2  47438  line2xlem  47439  line2x  47440  line2y  47441  itscnhlinecirc02p  47471  inlinecirc02plem  47472