Theorem 1ex 11103

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ℂcc 10999  1c1 11002

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 2113  ax-9 2121  ax-ext 2703  ax-1cn 11059

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438

This theorem is referenced by:  1nn  12131  dfnn2  12133  nn1suc  12142  nn0ind-raph  12568  fzprval  13480  fztpval  13481  expval  13965  m1expcl2  13987  1exp  13993  facnn  14177  fac0  14178  prhash2ex  14301  funcnvs2  14815  funcnvs3  14816  funcnvs4  14817  wrdlen2i  14844  wrd2pr2op  14845  wrd3tpop  14850  wwlktovf1  14859  wrdl3s3  14864  relexp1g  14928  dfid6  14930  sgnval  14990  harmonic  15761  prodf1f  15794  fprodntriv  15844  prod1  15846  fprodss  15850  fprodn0f  15893  ege2le3  15992  ruclem8  16141  ruclem11  16144  1nprm  16585  pcmpt  16799  smndex2dnrinv  18818  mgmnsgrpex  18834  pmtrprfval  19394  pmtrprfvalrn  19395  psgnprfval  19428  psgnprfval1  19429  abvtrivd  20742  pzriprng1ALT  21428  cnmsgnsubg  21509  psdmplcl  22072  psdmul  22076  psdmvr  22079  m2detleiblem1  22534  m2detleiblem5  22535  m2detleiblem6  22536  m2detleiblem3  22539  m2detleiblem4  22540  m2detleib  22541  imasdsf1olem  24283  pcopt  24944  pcopt2  24945  pcoass  24946  ehl1eudis  25342  ehl2eudis  25344  voliunlem1  25473  i1f1lem  25612  i1f1  25613  itg11  25614  iblcnlem1  25711  bddibl  25763  dvexp  25879  dvef  25906  mvth  25919  iaa  26255  aalioulem2  26263  efrlim  26901  efrlimOLD  26902  amgmlem  26922  amgm  26923  wilthlem2  27001  wilthlem3  27002  basellem7  27019  basellem9  27021  ppiublem2  27136  pclogsum  27148  bposlem5  27221  lgsfval  27235  lgsdir2lem3  27260  lgsdir  27265  lgsdilem2  27266  lgsdi  27267  lgsne0  27268  addsqnreup  27376  ostth1  27566  istrkg2ld  28433  axlowdimlem4  28918  axlowdimlem6  28920  axlowdimlem10  28924  axlowdimlem11  28925  axlowdimlem12  28926  axlowdimlem13  28927  axlowdim1  28932  umgr2v2eedg  29498  umgr2v2e  29499  umgr2v2evd2  29501  2wlklem  29639  usgr2trlncl  29733  2wlkdlem4  29901  2wlkdlem5  29902  2pthdlem1  29903  2wlkdlem10  29908  wwlks2onv  29926  elwwlks2ons3im  29927  umgrwwlks2on  29930  3wlkdlem4  30134  3wlkdlem5  30135  3pthdlem1  30136  3wlkdlem10  30141  upgr3v3e3cycl  30152  upgr4cycl4dv4e  30157  konigsberglem4  30227  konigsberglem5  30228  ex-xp  30408  nmopun  31986  pjnmopi  32120  iuninc  32532  fprodex01  32800  sgncl  32806  s2rnOLD  32917  s3rnOLD  32919  psgnid  33058  cyc3fv2  33099  cnmsgn0g  33107  cyc3evpm  33111  sgnsval  33122  sgnsf  33123  1fldgenq  33280  gsumind  33302  constrconj  33750  nn0constr  33766  cntnevol  34233  ddeval1  34239  ddeval0  34240  eulerpartgbij  34377  coinfliprv  34488  prodfzo03  34608  circlevma  34647  circlemethhgt  34648  hgt750lemg  34659  hgt750lemb  34661  hgt750lema  34662  hgt750leme  34663  tgoldbachgtde  34665  tgoldbachgt  34668  subfacp1lem1  35215  subfacp1lem2a  35216  subfacp1lem3  35218  subfacp1lem5  35220  cvmliftlem10  35330  sinccvglem  35708  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem10  37670  poimirlem11  37671  poimirlem12  37672  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem28  37688  poimirlem29  37689  poimirlem31  37691  itg2addnclem  37711  sticksstones11  42189  readvrec  42395  rabren3dioph  42848  2nn0ind  42978  flcidc  43203  dfrcl4  43709  fvilbdRP  43723  fvrcllb1d  43728  iunrelexp0  43735  corclrcl  43740  relexp1idm  43747  cotrcltrcl  43758  trclfvdecomr  43761  corcltrcl  43772  cotrclrcl  43775  dvsid  44364  binomcxplemnotnn0  44389  refsum2cnlem1  45074  infleinf  45410  itgsin0pilem1  45988  fourierdlem29  46174  fourierdlem56  46200  fourierdlem62  46206  fourierswlem  46268  fouriersw  46269  lamberte  46919  cjnpoly  46920  fun2dmnopgexmpl  47315  sbgoldbo  47818  nnsum3primes4  47819  nnsum3primesgbe  47823  nnsum4primesodd  47827  nnsum4primesoddALTV  47828  cycl3grtrilem  47977  stgr1  47992  usgrexmpl1lem  48052  usgrexmpl1tri  48056  usgrexmpl2lem  48057  usgrexmpl2nb0  48062  usgrexmpl2nb1  48063  usgrexmpl2nb2  48064  usgrexmpl2trifr  48068  gpgiedgdmellem  48077  gpgvtx1  48085  opgpgvtx  48086  gpgedgvtx1  48093  gpgvtxedg0  48094  gpgvtxedg1  48095  gpgedgiov  48096  gpgedg2iv  48098  gpg5nbgrvtx03starlem1  48099  gpg5nbgrvtx03starlem3  48101  gpg5nbgrvtx13starlem1  48102  gpg5nbgrvtx13starlem2  48103  gpg5nbgrvtx13starlem3  48104  gpg3nbgrvtx0  48107  gpg3nbgrvtx0ALT  48108  gpg3nbgrvtx1  48109  gpgcubic  48110  gpg5nbgr3star  48112  gpg3kgrtriex  48120  gpgprismgr4cycllem2  48127  gpgprismgr4cycllem3  48128  gpgprismgr4cycllem7  48132  gpgprismgr4cycllem9  48134  pgnioedg1  48139  pgnioedg2  48140  pgnioedg3  48141  pgnioedg4  48142  pgnioedg5  48143  pgnbgreunbgrlem2lem1  48145  pgnbgreunbgrlem2lem2  48146  pgnbgreunbgrlem2lem3  48147  pgnbgreunbgrlem2  48148  pgnbgreunbgrlem3  48149  pgnbgreunbgrlem4  48150  pgnbgreunbgrlem5lem1  48151  pgnbgreunbgrlem5lem2  48152  pgnbgreunbgrlem5lem3  48153  pgnbgreunbgrlem6  48155  gpg5edgnedg  48161  grlimedgnedg  48162  zlmodzxzel  48386  zlmodzxz0  48387  zlmodzxzscm  48388  zlmodzxzadd  48389  blenval  48603  nn0sumshdiglemB  48652  fv2arycl  48680  2arympt  48681  2arymptfv  48682  2arymaptf1  48685  2arymaptfo  48686  fv1prop  48731  rrx2pxel  48743  prelrrx2  48745  prelrrx2b  48746  rrx2pnecoorneor  48747  rrx2xpref1o  48750  rrx2plordisom  48755  ehl2eudisval0  48757  rrx2line  48772  rrx2linest  48774  rrx2linesl  48775  2sphere0  48782  line2ylem  48783  line2  48784  line2xlem  48785  line2x  48786  line2y  48787  itscnhlinecirc02p  48817  inlinecirc02plem  48818