Theorem 1ex 11227

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ℂcc 11122  1c1 11125

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 2732  ax-1cn 11182

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452

This theorem is used by:  1elpr01  11228  1nn  12268  dfnn2  12270  nn1suc  12279  1eltp012  12335  nn0ind-raph  12721  fzprval  13640  fztpval  13641  expval  14127  m1expcl2  14149  1exp  14155  facnn  14339  fac0  14340  prhash2ex  14463  funcnvs2  14984  funcnvs3  14985  funcnvs4  14986  wrdlen2i  15013  wrd2pr2op  15014  wrd3tpop  15019  wwlktovf1  15030  relexp1g  15099  dfid6  15101  sgnval  15161  sgndm  15169  sgncl  15170  harmonic  15948  prodf1f  15981  fprodntriv  16029  prod1  16031  fprodss  16035  fprodn0f  16078  ege2le3  16176  ruclem8  16325  ruclem11  16328  1nprm  16769  pcmpt  16984  smndex2dnrinv  19027  mgmnsgrpex  19043  pmtrprfval  19614  pmtrprfvalrn  19615  psgnprfval  19648  psgnprfval1  19649  abvtrivd  20998  pzriprng1ALT  21709  cnmsgnsubg  21790  psdmplcl  22390  psdmul  22394  psdmvr  22397  m2detleiblem1  22846  m2detleiblem5  22847  m2detleiblem6  22848  m2detleiblem3  22851  m2detleiblem4  22852  m2detleib  22853  imasdsf1olem  24599  pcopt  25250  pcopt2  25251  pcoass  25252  ehl1eudis  25648  ehl2eudis  25650  voliunlem1  25778  i1f1lem  25917  itg11  25919  iblcnlem1  26015  bddibl  26067  dvexp  26180  dvef  26207  mvth  26219  iaaOLD  26561  aalioulem2  26569  efrlim  27206  amgmlem  27226  amgm  27227  wilthlem2  27305  wilthlem3  27306  basellem7  27323  basellem9  27325  ppiublem2  27439  pclogsum  27451  bposlem5  27524  lgsfval  27538  lgsdir2lem3  27563  lgsdir  27568  lgsdilem2  27569  lgsdi  27570  lgsne0  27571  addsqnreup  27679  ostth1  27869  istrkg2ld  28801  axlowdimlem4  29402  axlowdimlem6  29404  axlowdimlem10  29408  axlowdimlem11  29409  axlowdimlem12  29410  axlowdimlem13  29411  axlowdim1  29416  umgr2v2eedg  29984  umgr2v2e  29985  umgr2v2evd2  29987  2wlklem  30125  usgr2trlncl  30225  2wlkdlem4  30396  2wlkdlem5  30397  2pthdlem1  30398  2wlkdlem10  30403  3wlkdlem4  30642  3wlkdlem5  30643  3pthdlem1  30644  3wlkdlem10  30649  upgr3v3e3cycl  30660  upgr4cycl4dv4e  30665  konigsberglem4  30735  konigsberglem5  30736  ex-xp  30916  nmopun  32495  pjnmopi  32629  iuninc  33034  fprodex01  33295  psgnid  33537  cnmsgn0g  33586  cyc3evpm  33590  sgnsval  33601  sgnsf  33602  1fldgenq  33763  gsumind  33785  cntnevol  34739  ddeval1  34745  ddeval0  34746  eulerpartgbij  34883  coinfliprv  34994  hgt750lemg  35162  hgt750lemb  35164  tgoldbachgt  35171  subfacp1lem1  35758  subfacp1lem2a  35759  subfacp1lem3  35761  subfacp1lem5  35763  cvmliftlem10  35873  sinccvglem  36251  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem4  38373  poimirlem6  38375  poimirlem7  38376  poimirlem10  38379  poimirlem11  38380  poimirlem12  38381  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem23  38392  poimirlem24  38393  poimirlem25  38394  poimirlem28  38397  poimirlem29  38398  poimirlem31  38400  itg2addnclem  38420  sticksstones11  43022  readvrec  43237  rabren3dioph  43656  2nn0ind  43786  flcidc  44011  dfrcl4  44516  fvilbdRP  44530  iunrelexp0  44542  corclrcl  44547  cotrcltrcl  44565  trclfvdecomr  44568  corcltrcl  44579  cotrclrcl  44582  dvsid  45155  binomcxplemnotnn0  45180  refsum2cnlem1  45871  infleinf  46201  itgsin0pilem1  46778  fourierdlem29  46964  fourierdlem56  46990  fourierdlem62  46996  fourierswlem  47058  fouriersw  47059  numtowerdt  47734  lamberte  47756  cjnpoly  47757  fun2dmnopgexmpl  48172  sbgoldbo  48703  nnsum3primes4  48704  nnsum3primesgbe  48708  nnsum4primesodd  48712  nnsum4primesoddALTV  48713  cycl3grtrilem  48862  stgr1  48877  usgrexmpl1lem  48937  usgrexmpl2lem  48942  usgrexmpl2nb0  48947  usgrexmpl2nb2  48949  usgrexmpl2trifr  48953  opgpgvtx  48971  gpgedgvtx1  48978  gpgvtxedg0  48979  gpgvtxedg1  48980  gpgedgiov  48981  gpgedg2iv  48983  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg3nbgrvtx0  48992  gpg3nbgrvtx0ALT  48993  gpg3nbgrvtx1  48994  gpgcubic  48995  gpg5nbgr3star  48997  gpg3kgrtriex  49005  gpgprismgr4cycllem2  49012  gpgprismgr4cycllem7  49017  pgnioedg1  49024  pgnioedg2  49025  pgnioedg3  49026  pgnioedg4  49027  pgnioedg5  49028  pgnbgreunbgrlem2lem1  49030  pgnbgreunbgrlem2lem2  49031  pgnbgreunbgrlem2lem3  49032  pgnbgreunbgrlem2  49033  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem4  49035  pgnbgreunbgrlem5lem1  49036  pgnbgreunbgrlem5lem2  49037  pgnbgreunbgrlem5lem3  49038  pgnbgreunbgrlem6  49040  gpg5edgnedg  49046  zlmodzxzel  49285  zlmodzxz0  49286  zlmodzxzscm  49287  zlmodzxzadd  49288  blenval  49501  nn0sumshdiglemB  49550  fv2arycl  49578  2arymptfv  49580  2arymaptf1  49583  2arymaptfo  49584  fv1prop  49629  rrx2pxel  49641  prelrrx2  49643  prelrrx2b  49644  rrx2pnecoorneor  49645  rrx2xpref1o  49648  rrx2plordisom  49653  ehl2eudisval0  49655  rrx2line  49670  rrx2linest  49672  rrx2linesl  49673  2sphere0  49680  line2ylem  49681  line2  49682  line2xlem  49683  line2x  49684  line2y  49685  itscnhlinecirc02p  49715  inlinecirc02plem  49716