Theorem 1ex 11214

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ℂcc 11109  1c1 11112

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 2148  ax-9 2156  ax-ext 2737  ax-1cn 11169

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459

This theorem is used by:  1elpr01  11215  1nn  12255  dfnn2  12257  nn1suc  12266  1eltp012  12322  nn0ind-raph  12708  fzprval  13626  fztpval  13627  expval  14113  m1expcl2  14135  1exp  14141  facnn  14325  fac0  14326  prhash2ex  14449  funcnvs2  14970  funcnvs3  14971  funcnvs4  14972  wrdlen2i  14999  wrd2pr2op  15000  wrd3tpop  15005  wwlktovf1  15014  relexp1g  15083  dfid6  15085  sgnval  15145  sgndm  15153  sgncl  15154  harmonic  15932  prodf1f  15965  fprodntriv  16015  prod1  16017  fprodss  16021  fprodn0f  16064  ege2le3  16162  ruclem8  16311  ruclem11  16314  1nprm  16755  pcmpt  16970  smndex2dnrinv  19001  mgmnsgrpex  19017  pmtrprfval  19581  pmtrprfvalrn  19582  psgnprfval  19615  psgnprfval1  19616  abvtrivd  20965  pzriprng1ALT  21676  cnmsgnsubg  21757  psdmplcl  22355  psdmul  22359  psdmvr  22362  m2detleiblem1  22811  m2detleiblem5  22812  m2detleiblem6  22813  m2detleiblem3  22816  m2detleiblem4  22817  m2detleib  22818  imasdsf1olem  24561  pcopt  25212  pcopt2  25213  pcoass  25214  ehl1eudis  25610  ehl2eudis  25612  voliunlem1  25740  i1f1lem  25879  itg11  25881  iblcnlem1  25978  bddibl  26030  dvexp  26143  dvef  26170  mvth  26182  iaa  26519  aalioulem2  26527  efrlim  27165  amgmlem  27185  amgm  27186  wilthlem2  27264  wilthlem3  27265  basellem7  27282  basellem9  27284  ppiublem2  27398  pclogsum  27410  bposlem5  27483  lgsfval  27497  lgsdir2lem3  27522  lgsdir  27527  lgsdilem2  27528  lgsdi  27529  lgsne0  27530  addsqnreup  27638  ostth1  27828  istrkg2ld  28760  axlowdimlem4  29326  axlowdimlem6  29328  axlowdimlem10  29332  axlowdimlem11  29333  axlowdimlem12  29334  axlowdimlem13  29335  axlowdim1  29340  umgr2v2eedg  29908  umgr2v2e  29909  umgr2v2evd2  29911  2wlklem  30049  usgr2trlncl  30149  2wlkdlem4  30320  2wlkdlem5  30321  2pthdlem1  30322  2wlkdlem10  30327  3wlkdlem4  30560  3wlkdlem5  30561  3pthdlem1  30562  3wlkdlem10  30567  upgr3v3e3cycl  30578  upgr4cycl4dv4e  30583  konigsberglem4  30653  konigsberglem5  30654  ex-xp  30834  nmopun  32413  pjnmopi  32547  iuninc  32952  fprodex01  33215  psgnid  33457  cnmsgn0g  33506  cyc3evpm  33510  sgnsval  33521  sgnsf  33522  1fldgenq  33683  gsumind  33705  cntnevol  34659  ddeval1  34665  ddeval0  34666  eulerpartgbij  34803  coinfliprv  34914  hgt750lemg  35082  hgt750lemb  35084  tgoldbachgt  35091  subfacp1lem1  35684  subfacp1lem2a  35685  subfacp1lem3  35687  subfacp1lem5  35689  cvmliftlem10  35799  sinccvglem  36177  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem7  38311  poimirlem10  38314  poimirlem11  38315  poimirlem12  38316  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem28  38332  poimirlem29  38333  poimirlem31  38335  itg2addnclem  38355  sticksstones11  42956  readvrec  43156  rabren3dioph  43575  2nn0ind  43705  flcidc  43930  dfrcl4  44435  fvilbdRP  44449  iunrelexp0  44461  corclrcl  44466  cotrcltrcl  44484  trclfvdecomr  44487  corcltrcl  44498  cotrclrcl  44501  dvsid  45074  binomcxplemnotnn0  45099  refsum2cnlem1  45790  infleinf  46120  itgsin0pilem1  46697  fourierdlem29  46883  fourierdlem56  46909  fourierdlem62  46915  fourierswlem  46977  fouriersw  46978  nthrucw  47640  lamberte  47658  cjnpoly  47659  fun2dmnopgexmpl  48054  sbgoldbo  48585  nnsum3primes4  48586  nnsum3primesgbe  48590  nnsum4primesodd  48594  nnsum4primesoddALTV  48595  cycl3grtrilem  48744  stgr1  48759  usgrexmpl1lem  48819  usgrexmpl2lem  48824  usgrexmpl2nb0  48829  usgrexmpl2nb2  48831  usgrexmpl2trifr  48835  opgpgvtx  48853  gpgedgvtx1  48860  gpgvtxedg0  48861  gpgvtxedg1  48862  gpgedgiov  48863  gpgedg2iv  48865  gpg5nbgrvtx03starlem1  48866  gpg5nbgrvtx03starlem3  48868  gpg5nbgrvtx13starlem1  48869  gpg5nbgrvtx13starlem2  48870  gpg5nbgrvtx13starlem3  48871  gpg3nbgrvtx0  48874  gpg3nbgrvtx0ALT  48875  gpg3nbgrvtx1  48876  gpgcubic  48877  gpg5nbgr3star  48879  gpg3kgrtriex  48887  gpgprismgr4cycllem2  48894  gpgprismgr4cycllem7  48899  pgnioedg1  48906  pgnioedg2  48907  pgnioedg3  48908  pgnioedg4  48909  pgnioedg5  48910  pgnbgreunbgrlem2lem1  48912  pgnbgreunbgrlem2lem2  48913  pgnbgreunbgrlem2lem3  48914  pgnbgreunbgrlem2  48915  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem4  48917  pgnbgreunbgrlem5lem1  48918  pgnbgreunbgrlem5lem2  48919  pgnbgreunbgrlem5lem3  48920  pgnbgreunbgrlem6  48922  gpg5edgnedg  48928  zlmodzxzel  49168  zlmodzxz0  49169  zlmodzxzscm  49170  zlmodzxzadd  49171  blenval  49384  nn0sumshdiglemB  49433  fv2arycl  49461  2arymptfv  49463  2arymaptf1  49466  2arymaptfo  49467  fv1prop  49512  rrx2pxel  49524  prelrrx2  49526  prelrrx2b  49527  rrx2pnecoorneor  49528  rrx2xpref1o  49531  rrx2plordisom  49536  ehl2eudisval0  49538  rrx2line  49553  rrx2linest  49555  rrx2linesl  49556  2sphere0  49563  line2ylem  49564  line2  49565  line2xlem  49566  line2x  49567  line2y  49568  itscnhlinecirc02p  49598  inlinecirc02plem  49599