Theorem 1ex 11177

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

Syntax hints:   ∈ wcel 2109  Vcvv 3450  ℂcc 11073  1c1 11076

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-1cn 11133

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452

This theorem is referenced by:  1nn  12204  dfnn2  12206  nn1suc  12215  nn0ind-raph  12641  fzprval  13553  fztpval  13554  expval  14035  m1expcl2  14057  1exp  14063  facnn  14247  fac0  14248  prhash2ex  14371  funcnvs2  14886  funcnvs3  14887  funcnvs4  14888  wrdlen2i  14915  wrd2pr2op  14916  wrd3tpop  14921  wwlktovf1  14930  wrdl3s3  14935  relexp1g  14999  dfid6  15001  sgnval  15061  harmonic  15832  prodf1f  15865  fprodntriv  15915  prod1  15917  fprodss  15921  fprodn0f  15964  ege2le3  16063  ruclem8  16212  ruclem11  16215  1nprm  16656  pcmpt  16870  smndex2dnrinv  18849  mgmnsgrpex  18865  pmtrprfval  19424  pmtrprfvalrn  19425  psgnprfval  19458  psgnprfval1  19459  abvtrivd  20748  pzriprng1ALT  21413  cnmsgnsubg  21493  psdmplcl  22056  psdmul  22060  psdmvr  22063  m2detleiblem1  22518  m2detleiblem5  22519  m2detleiblem6  22520  m2detleiblem3  22523  m2detleiblem4  22524  m2detleib  22525  imasdsf1olem  24268  pcopt  24929  pcopt2  24930  pcoass  24931  ehl1eudis  25327  ehl2eudis  25329  voliunlem1  25458  i1f1lem  25597  i1f1  25598  itg11  25599  iblcnlem1  25696  bddibl  25748  dvexp  25864  dvef  25891  mvth  25904  iaa  26240  aalioulem2  26248  efrlim  26886  efrlimOLD  26887  amgmlem  26907  amgm  26908  wilthlem2  26986  wilthlem3  26987  basellem7  27004  basellem9  27006  ppiublem2  27121  pclogsum  27133  bposlem5  27206  lgsfval  27220  lgsdir2lem3  27245  lgsdir  27250  lgsdilem2  27251  lgsdi  27252  lgsne0  27253  addsqnreup  27361  ostth1  27551  istrkg2ld  28394  axlowdimlem4  28879  axlowdimlem6  28881  axlowdimlem10  28885  axlowdimlem11  28886  axlowdimlem12  28887  axlowdimlem13  28888  axlowdim1  28893  umgr2v2eedg  29459  umgr2v2e  29460  umgr2v2evd2  29462  2wlklem  29602  usgr2trlncl  29697  2wlkdlem4  29865  2wlkdlem5  29866  2pthdlem1  29867  2wlkdlem10  29872  wwlks2onv  29890  elwwlks2ons3im  29891  umgrwwlks2on  29894  3wlkdlem4  30098  3wlkdlem5  30099  3pthdlem1  30100  3wlkdlem10  30105  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  konigsberglem4  30191  konigsberglem5  30192  ex-xp  30372  nmopun  31950  pjnmopi  32084  iuninc  32496  fprodex01  32757  sgncl  32763  s2rnOLD  32872  s3rnOLD  32874  psgnid  33061  cyc3fv2  33102  cnmsgn0g  33110  cyc3evpm  33114  sgnsval  33125  sgnsf  33126  1fldgenq  33279  constrconj  33742  nn0constr  33758  cntnevol  34225  ddeval1  34231  ddeval0  34232  eulerpartgbij  34370  coinfliprv  34481  prodfzo03  34601  circlevma  34640  circlemethhgt  34641  hgt750lemg  34652  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgt  34661  subfacp1lem1  35173  subfacp1lem2a  35174  subfacp1lem3  35176  subfacp1lem5  35178  cvmliftlem10  35288  sinccvglem  35666  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  itg2addnclem  37672  sticksstones11  42151  readvrec  42357  rabren3dioph  42810  2nn0ind  42941  flcidc  43166  dfrcl4  43672  fvilbdRP  43686  fvrcllb1d  43691  iunrelexp0  43698  corclrcl  43703  relexp1idm  43710  cotrcltrcl  43721  trclfvdecomr  43724  corcltrcl  43735  cotrclrcl  43738  dvsid  44327  binomcxplemnotnn0  44352  refsum2cnlem1  45038  infleinf  45375  itgsin0pilem1  45955  fourierdlem29  46141  fourierdlem56  46167  fourierdlem62  46173  fourierswlem  46235  fouriersw  46236  lamberte  46896  fun2dmnopgexmpl  47289  sbgoldbo  47792  nnsum3primes4  47793  nnsum3primesgbe  47797  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  cycl3grtrilem  47949  stgr1  47964  usgrexmpl1lem  48016  usgrexmpl1tri  48020  usgrexmpl2lem  48021  usgrexmpl2nb0  48026  usgrexmpl2nb1  48027  usgrexmpl2nb2  48028  usgrexmpl2trifr  48032  gpgiedgdmellem  48041  gpgvtx1  48049  opgpgvtx  48050  gpgedgvtx1  48057  gpgvtxedg0  48058  gpgvtxedg1  48059  gpgedgiov  48060  gpgedg2iv  48062  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  gpg3nbgrvtx0  48071  gpg3nbgrvtx0ALT  48072  gpg3nbgrvtx1  48073  gpgcubic  48074  gpg5nbgr3star  48076  gpg3kgrtriex  48084  gpgprismgr4cycllem2  48090  gpgprismgr4cycllem3  48091  gpgprismgr4cycllem7  48095  gpgprismgr4cycllem9  48097  pgnioedg1  48102  pgnioedg2  48103  pgnioedg3  48104  pgnioedg4  48105  pgnioedg5  48106  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  pgnbgreunbgrlem2lem3  48110  pgnbgreunbgrlem2  48111  pgnbgreunbgrlem3  48112  pgnbgreunbgrlem4  48113  pgnbgreunbgrlem5lem1  48114  pgnbgreunbgrlem5lem2  48115  pgnbgreunbgrlem5lem3  48116  pgnbgreunbgrlem6  48118  zlmodzxzel  48347  zlmodzxz0  48348  zlmodzxzscm  48349  zlmodzxzadd  48350  blenval  48564  nn0sumshdiglemB  48613  fv2arycl  48641  2arympt  48642  2arymptfv  48643  2arymaptf1  48646  2arymaptfo  48647  fv1prop  48692  rrx2pxel  48704  prelrrx2  48706  prelrrx2b  48707  rrx2pnecoorneor  48708  rrx2xpref1o  48711  rrx2plordisom  48716  ehl2eudisval0  48718  rrx2line  48733  rrx2linest  48735  rrx2linesl  48736  2sphere0  48743  line2ylem  48744  line2  48745  line2xlem  48746  line2x  48747  line2y  48748  itscnhlinecirc02p  48778  inlinecirc02plem  48779