Theorem 1ex 11229

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

Syntax hints:   ∈ wcel 2108  Vcvv 3459  ℂcc 11125  1c1 11128

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-1cn 11185

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461

This theorem is referenced by:  1nn  12249  dfnn2  12251  nn1suc  12260  nn0ind-raph  12691  fzprval  13600  fztpval  13601  expval  14079  m1expcl2  14101  1exp  14107  facnn  14291  fac0  14292  prhash2ex  14415  funcnvs2  14930  funcnvs3  14931  funcnvs4  14932  wrdlen2i  14959  wrd2pr2op  14960  wrd3tpop  14965  wwlktovf1  14974  wrdl3s3  14979  relexp1g  15043  dfid6  15045  sgnval  15105  harmonic  15873  prodf1f  15906  fprodntriv  15956  prod1  15958  fprodss  15962  fprodn0f  16005  ege2le3  16104  ruclem8  16253  ruclem11  16256  1nprm  16696  pcmpt  16910  smndex2dnrinv  18891  mgmnsgrpex  18907  pmtrprfval  19466  pmtrprfvalrn  19467  psgnprfval  19500  psgnprfval1  19501  abvtrivd  20790  pzriprng1ALT  21455  cnmsgnsubg  21535  psdmplcl  22098  psdmul  22102  psdmvr  22105  m2detleiblem1  22560  m2detleiblem5  22561  m2detleiblem6  22562  m2detleiblem3  22565  m2detleiblem4  22566  m2detleib  22567  imasdsf1olem  24310  pcopt  24971  pcopt2  24972  pcoass  24973  ehl1eudis  25370  ehl2eudis  25372  voliunlem1  25501  i1f1lem  25640  i1f1  25641  itg11  25642  iblcnlem1  25739  bddibl  25791  dvexp  25907  dvef  25934  mvth  25947  iaa  26283  aalioulem2  26291  efrlim  26929  efrlimOLD  26930  amgmlem  26950  amgm  26951  wilthlem2  27029  wilthlem3  27030  basellem7  27047  basellem9  27049  ppiublem2  27164  pclogsum  27176  bposlem5  27249  lgsfval  27263  lgsdir2lem3  27288  lgsdir  27293  lgsdilem2  27294  lgsdi  27295  lgsne0  27296  addsqnreup  27404  ostth1  27594  istrkg2ld  28385  axlowdimlem4  28870  axlowdimlem6  28872  axlowdimlem10  28876  axlowdimlem11  28877  axlowdimlem12  28878  axlowdimlem13  28879  axlowdim1  28884  umgr2v2eedg  29450  umgr2v2e  29451  umgr2v2evd2  29453  2wlklem  29593  usgr2trlncl  29688  2wlkdlem4  29856  2wlkdlem5  29857  2pthdlem1  29858  2wlkdlem10  29863  wwlks2onv  29881  elwwlks2ons3im  29882  umgrwwlks2on  29885  3wlkdlem4  30089  3wlkdlem5  30090  3pthdlem1  30091  3wlkdlem10  30096  upgr3v3e3cycl  30107  upgr4cycl4dv4e  30112  konigsberglem4  30182  konigsberglem5  30183  ex-xp  30363  nmopun  31941  pjnmopi  32075  iuninc  32487  fprodex01  32750  sgncl  32756  s2rnOLD  32865  s3rnOLD  32867  psgnid  33054  cyc3fv2  33095  cnmsgn0g  33103  cyc3evpm  33107  sgnsval  33118  sgnsf  33119  1fldgenq  33262  constrconj  33725  nn0constr  33741  cntnevol  34205  ddeval1  34211  ddeval0  34212  eulerpartgbij  34350  coinfliprv  34461  prodfzo03  34581  circlevma  34620  circlemethhgt  34621  hgt750lemg  34632  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgt  34641  subfacp1lem1  35147  subfacp1lem2a  35148  subfacp1lem3  35150  subfacp1lem5  35152  cvmliftlem10  35262  sinccvglem  35640  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem4  37594  poimirlem6  37596  poimirlem7  37597  poimirlem10  37600  poimirlem11  37601  poimirlem12  37602  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem23  37613  poimirlem24  37614  poimirlem25  37615  poimirlem28  37618  poimirlem29  37619  poimirlem31  37621  itg2addnclem  37641  sticksstones11  42115  readvrec  42352  rabren3dioph  42785  2nn0ind  42916  flcidc  43141  dfrcl4  43647  fvilbdRP  43661  fvrcllb1d  43666  iunrelexp0  43673  corclrcl  43678  relexp1idm  43685  cotrcltrcl  43696  trclfvdecomr  43699  corcltrcl  43710  cotrclrcl  43713  dvsid  44303  binomcxplemnotnn0  44328  refsum2cnlem1  45009  infleinf  45347  itgsin0pilem1  45927  fourierdlem29  46113  fourierdlem56  46139  fourierdlem62  46145  fourierswlem  46207  fouriersw  46208  lamberte  46868  fun2dmnopgexmpl  47261  sbgoldbo  47749  nnsum3primes4  47750  nnsum3primesgbe  47754  nnsum4primesodd  47758  nnsum4primesoddALTV  47759  cycl3grtrilem  47906  stgr1  47921  usgrexmpl1lem  47973  usgrexmpl1tri  47977  usgrexmpl2lem  47978  usgrexmpl2nb0  47983  usgrexmpl2nb1  47984  usgrexmpl2nb2  47985  usgrexmpl2trifr  47989  gpgiedgdmellem  47998  gpgvtx1  48006  opgpgvtx  48007  gpgedgvtx1  48014  gpgvtxedg0  48015  gpgvtxedg1  48016  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  gpg3nbgrvtx0  48026  gpg3nbgrvtx0ALT  48027  gpg3nbgrvtx1  48028  gpgcubic  48029  gpg5nbgr3star  48031  gpg3kgrtriex  48039  gpgprismgr4cycllem2  48043  gpgprismgr4cycllem3  48044  gpgprismgr4cycllem7  48048  gpgprismgr4cycllem9  48050  zlmodzxzel  48278  zlmodzxz0  48279  zlmodzxzscm  48280  zlmodzxzadd  48281  blenval  48499  nn0sumshdiglemB  48548  fv2arycl  48576  2arympt  48577  2arymptfv  48578  2arymaptf1  48581  2arymaptfo  48582  fv1prop  48627  rrx2pxel  48639  prelrrx2  48641  prelrrx2b  48642  rrx2pnecoorneor  48643  rrx2xpref1o  48646  rrx2plordisom  48651  ehl2eudisval0  48653  rrx2line  48668  rrx2linest  48670  rrx2linesl  48671  2sphere0  48678  line2ylem  48679  line2  48680  line2xlem  48681  line2x  48682  line2y  48683  itscnhlinecirc02p  48713  inlinecirc02plem  48714