Theorem 1ex 11296

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ℂcc 11191  1c1 11194

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-1cn 11251

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453

This theorem is used by:  1elpr01  11297  1nn  12339  dfnn2  12341  nn1suc  12350  1eltp012  12406  nn0ind-raph  12792  fzprval  13712  fztpval  13713  expval  14199  m1expcl2  14221  1exp  14227  facnn  14412  fac0  14413  prhash2ex  14536  funcnvs2  15057  funcnvs3  15058  funcnvs4  15059  wrdlen2i  15086  wrd2pr2op  15087  wrd3tpop  15092  wwlktovf1  15103  relexp1g  15172  dfid6  15174  sgnval  15234  sgndm  15242  sgncl  15243  harmonic  16021  prodf1f  16054  fprodntriv  16102  prod1  16104  fprodss  16108  fprodn0f  16151  ege2le3  16249  ruclem8  16398  ruclem11  16401  1nprm  16847  pcmpt  17063  smndex2dnrinv  19107  mgmnsgrpex  19123  pmtrprfval  19694  pmtrprfvalrn  19695  psgnprfval  19728  psgnprfval1  19729  abvtrivd  21082  pzriprng1ALT  21795  cnmsgnsubg  21876  psdmplcl  22476  psdmul  22480  psdmvr  22483  m2detleiblem1  22932  m2detleiblem5  22933  m2detleiblem6  22934  m2detleiblem3  22937  m2detleiblem4  22938  m2detleib  22939  imasdsf1olem  24685  pcopt  25336  pcopt2  25337  pcoass  25338  ehl1eudis  25734  ehl2eudis  25736  voliunlem1  25864  i1f1lem  26003  itg11  26005  iblcnlem1  26101  bddibl  26153  dvexp  26266  dvef  26293  mvth  26305  iaaOLD  26645  aalioulem2  26653  efrlim  27290  amgmlem  27310  amgm  27311  wilthlem2  27389  wilthlem3  27390  basellem7  27407  basellem9  27409  ppiublem2  27523  pclogsum  27535  bposlem5  27608  lgsfval  27622  lgsdir2lem3  27647  lgsdir  27652  lgsdilem2  27653  lgsdi  27654  lgsne0  27655  addsqnreup  27763  ostth1  27953  istrkg2ld  28915  axlowdimlem4  29516  axlowdimlem6  29518  axlowdimlem10  29522  axlowdimlem11  29523  axlowdimlem12  29524  axlowdimlem13  29525  axlowdim1  29530  umgr2v2eedg  30098  umgr2v2e  30099  umgr2v2evd2  30101  2wlklem  30239  usgr2trlncl  30339  2wlkdlem4  30510  2wlkdlem5  30511  2pthdlem1  30512  2wlkdlem10  30517  3wlkdlem4  30756  3wlkdlem5  30757  3pthdlem1  30758  3wlkdlem10  30763  upgr3v3e3cycl  30774  upgr4cycl4dv4e  30779  konigsberglem4  30849  konigsberglem5  30850  ex-xp  31030  nmopun  32609  pjnmopi  32743  iuninc  33148  fprodex01  33409  psgnid  33651  cnmsgn0g  33700  cyc3evpm  33704  sgnsval  33715  sgnsf  33716  1fldgenq  33877  gsumind  33899  cntnevol  34854  ddeval1  34860  ddeval0  34861  eulerpartgbij  34997  coinfliprv  35108  hgt750lemg  35276  hgt750lemb  35278  tgoldbachgt  35285  subfacp1lem1  35923  subfacp1lem2a  35924  subfacp1lem3  35926  subfacp1lem5  35928  cvmliftlem10  36038  sinccvglem  36416  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem4  38522  poimirlem6  38524  poimirlem7  38525  poimirlem10  38528  poimirlem11  38529  poimirlem12  38530  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem23  38541  poimirlem24  38542  poimirlem25  38543  poimirlem28  38546  poimirlem29  38547  poimirlem31  38549  itg2addnclem  38569  sticksstones11  43186  readvrec  43393  rabren3dioph  43801  2nn0ind  43931  flcidc  44156  dfrcl4  44661  fvilbdRP  44675  iunrelexp0  44687  corclrcl  44692  cotrcltrcl  44710  trclfvdecomr  44713  corcltrcl  44724  cotrclrcl  44727  dvsid  45300  binomcxplemnotnn0  45325  refsum2cnlem1  46023  infleinf  46352  itgsin0pilem1  46929  fourierdlem29  47115  fourierdlem56  47141  fourierdlem62  47147  fourierswlem  47209  fouriersw  47210  numtowerdt  47885  lamberte  47907  cjnpoly  47908  fun2dmnopgexmpl  48323  sbgoldbo  48854  nnsum3primes4  48855  nnsum3primesgbe  48859  nnsum4primesodd  48863  nnsum4primesoddALTV  48864  cycl3grtrilem  49013  stgr1  49028  usgrexmpl1lem  49088  usgrexmpl2lem  49093  usgrexmpl2nb0  49098  usgrexmpl2nb2  49100  usgrexmpl2trifr  49104  opgpgvtx  49122  gpgedgvtx1  49129  gpgvtxedg0  49130  gpgvtxedg1  49131  gpgedgiov  49132  gpgedg2iv  49134  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg3nbgrvtx0  49143  gpg3nbgrvtx0ALT  49144  gpg3nbgrvtx1  49145  gpgcubic  49146  gpg5nbgr3star  49148  gpg3kgrtriex  49156  gpgprismgr4cycllem2  49163  gpgprismgr4cycllem7  49168  pgnioedg1  49175  pgnioedg2  49176  pgnioedg3  49177  pgnioedg4  49178  pgnioedg5  49179  pgnbgreunbgrlem2lem1  49181  pgnbgreunbgrlem2lem2  49182  pgnbgreunbgrlem2lem3  49183  pgnbgreunbgrlem2  49184  pgnbgreunbgrlem3  49185  pgnbgreunbgrlem4  49186  pgnbgreunbgrlem5lem1  49187  pgnbgreunbgrlem5lem2  49188  pgnbgreunbgrlem5lem3  49189  pgnbgreunbgrlem6  49191  gpg5edgnedg  49197  zlmodzxzel  49436  zlmodzxz0  49437  zlmodzxzscm  49438  zlmodzxzadd  49439  blenval  49652  nn0sumshdiglemB  49701  fv2arycl  49729  2arymptfv  49731  2arymaptf1  49734  2arymaptfo  49735  fv1prop  49780  rrx2pxel  49792  prelrrx2  49794  prelrrx2b  49795  rrx2pnecoorneor  49796  rrx2xpref1o  49799  rrx2plordisom  49804  ehl2eudisval0  49806  rrx2line  49821  rrx2linest  49823  rrx2linesl  49824  2sphere0  49831  line2ylem  49832  line2  49833  line2xlem  49834  line2x  49835  line2y  49836  itscnhlinecirc02p  49866  inlinecirc02plem  49867