Theorem 1ex 11128

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ℂcc 11024  1c1 11027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-1cn 11084

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442

This theorem is referenced by:  1nn  12156  dfnn2  12158  nn1suc  12167  nn0ind-raph  12592  fzprval  13501  fztpval  13502  expval  13986  m1expcl2  14008  1exp  14014  facnn  14198  fac0  14199  prhash2ex  14322  funcnvs2  14836  funcnvs3  14837  funcnvs4  14838  wrdlen2i  14865  wrd2pr2op  14866  wrd3tpop  14871  wwlktovf1  14880  wrdl3s3  14885  relexp1g  14949  dfid6  14951  sgnval  15011  harmonic  15782  prodf1f  15815  fprodntriv  15865  prod1  15867  fprodss  15871  fprodn0f  15914  ege2le3  16013  ruclem8  16162  ruclem11  16165  1nprm  16606  pcmpt  16820  smndex2dnrinv  18840  mgmnsgrpex  18856  pmtrprfval  19416  pmtrprfvalrn  19417  psgnprfval  19450  psgnprfval1  19451  abvtrivd  20765  pzriprng1ALT  21451  cnmsgnsubg  21532  psdmplcl  22105  psdmul  22109  psdmvr  22112  m2detleiblem1  22568  m2detleiblem5  22569  m2detleiblem6  22570  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  imasdsf1olem  24317  pcopt  24978  pcopt2  24979  pcoass  24980  ehl1eudis  25376  ehl2eudis  25378  voliunlem1  25507  i1f1lem  25646  i1f1  25647  itg11  25648  iblcnlem1  25745  bddibl  25797  dvexp  25913  dvef  25940  mvth  25953  iaa  26289  aalioulem2  26297  efrlim  26935  efrlimOLD  26936  amgmlem  26956  amgm  26957  wilthlem2  27035  wilthlem3  27036  basellem7  27053  basellem9  27055  ppiublem2  27170  pclogsum  27182  bposlem5  27255  lgsfval  27269  lgsdir2lem3  27294  lgsdir  27299  lgsdilem2  27300  lgsdi  27301  lgsne0  27302  addsqnreup  27410  ostth1  27600  istrkg2ld  28532  axlowdimlem4  29018  axlowdimlem6  29020  axlowdimlem10  29024  axlowdimlem11  29025  axlowdimlem12  29026  axlowdimlem13  29027  axlowdim1  29032  umgr2v2eedg  29598  umgr2v2e  29599  umgr2v2evd2  29601  2wlklem  29739  usgr2trlncl  29833  2wlkdlem4  30001  2wlkdlem5  30002  2pthdlem1  30003  2wlkdlem10  30008  wwlks2onv  30026  elwwlks2ons3im  30027  usgrwwlks2on  30031  umgrwwlks2on  30032  3wlkdlem4  30237  3wlkdlem5  30238  3pthdlem1  30239  3wlkdlem10  30244  upgr3v3e3cycl  30255  upgr4cycl4dv4e  30260  konigsberglem4  30330  konigsberglem5  30331  ex-xp  30511  nmopun  32089  pjnmopi  32223  iuninc  32635  fprodex01  32906  sgncl  32912  s2rnOLD  33026  s3rnOLD  33028  psgnid  33179  cyc3fv2  33220  cnmsgn0g  33228  cyc3evpm  33232  sgnsval  33243  sgnsf  33244  1fldgenq  33404  gsumind  33426  constrconj  33902  nn0constr  33918  cntnevol  34385  ddeval1  34391  ddeval0  34392  eulerpartgbij  34529  coinfliprv  34640  prodfzo03  34760  circlevma  34799  circlemethhgt  34800  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgt  34820  subfacp1lem1  35373  subfacp1lem2a  35374  subfacp1lem3  35376  subfacp1lem5  35378  cvmliftlem10  35488  sinccvglem  35866  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  itg2addnclem  37872  sticksstones11  42410  readvrec  42617  rabren3dioph  43057  2nn0ind  43187  flcidc  43412  dfrcl4  43917  fvilbdRP  43931  fvrcllb1d  43936  iunrelexp0  43943  corclrcl  43948  relexp1idm  43955  cotrcltrcl  43966  trclfvdecomr  43969  corcltrcl  43980  cotrclrcl  43983  dvsid  44572  binomcxplemnotnn0  44597  refsum2cnlem1  45282  infleinf  45616  itgsin0pilem1  46194  fourierdlem29  46380  fourierdlem56  46406  fourierdlem62  46412  fourierswlem  46474  fouriersw  46475  nthrucw  47130  lamberte  47134  cjnpoly  47135  fun2dmnopgexmpl  47530  sbgoldbo  48033  nnsum3primes4  48034  nnsum3primesgbe  48038  nnsum4primesodd  48042  nnsum4primesoddALTV  48043  cycl3grtrilem  48192  stgr1  48207  usgrexmpl1lem  48267  usgrexmpl1tri  48271  usgrexmpl2lem  48272  usgrexmpl2nb0  48277  usgrexmpl2nb1  48278  usgrexmpl2nb2  48279  usgrexmpl2trifr  48283  gpgiedgdmellem  48292  gpgvtx1  48300  opgpgvtx  48301  gpgedgvtx1  48308  gpgvtxedg0  48309  gpgvtxedg1  48310  gpgedgiov  48311  gpgedg2iv  48313  gpg5nbgrvtx03starlem1  48314  gpg5nbgrvtx03starlem3  48316  gpg5nbgrvtx13starlem1  48317  gpg5nbgrvtx13starlem2  48318  gpg5nbgrvtx13starlem3  48319  gpg3nbgrvtx0  48322  gpg3nbgrvtx0ALT  48323  gpg3nbgrvtx1  48324  gpgcubic  48325  gpg5nbgr3star  48327  gpg3kgrtriex  48335  gpgprismgr4cycllem2  48342  gpgprismgr4cycllem3  48343  gpgprismgr4cycllem7  48347  gpgprismgr4cycllem9  48349  pgnioedg1  48354  pgnioedg2  48355  pgnioedg3  48356  pgnioedg4  48357  pgnioedg5  48358  pgnbgreunbgrlem2lem1  48360  pgnbgreunbgrlem2lem2  48361  pgnbgreunbgrlem2lem3  48362  pgnbgreunbgrlem2  48363  pgnbgreunbgrlem3  48364  pgnbgreunbgrlem4  48365  pgnbgreunbgrlem5lem1  48366  pgnbgreunbgrlem5lem2  48367  pgnbgreunbgrlem5lem3  48368  pgnbgreunbgrlem6  48370  gpg5edgnedg  48376  grlimedgnedg  48377  zlmodzxzel  48601  zlmodzxz0  48602  zlmodzxzscm  48603  zlmodzxzadd  48604  blenval  48817  nn0sumshdiglemB  48866  fv2arycl  48894  2arympt  48895  2arymptfv  48896  2arymaptf1  48899  2arymaptfo  48900  fv1prop  48945  rrx2pxel  48957  prelrrx2  48959  prelrrx2b  48960  rrx2pnecoorneor  48961  rrx2xpref1o  48964  rrx2plordisom  48969  ehl2eudisval0  48971  rrx2line  48986  rrx2linest  48988  rrx2linesl  48989  2sphere0  48996  line2ylem  48997  line2  48998  line2xlem  48999  line2x  49000  line2y  49001  itscnhlinecirc02p  49031  inlinecirc02plem  49032