Theorem 1ex 11257

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

Syntax hints:   ∈ wcel 2108  Vcvv 3480  ℂcc 11153  1c1 11156

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-1cn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482

This theorem is referenced by:  1nn  12277  dfnn2  12279  nn1suc  12288  nn0ind-raph  12718  fzprval  13625  fztpval  13626  expval  14104  m1expcl2  14126  1exp  14132  facnn  14314  fac0  14315  prhash2ex  14438  funcnvs2  14952  funcnvs3  14953  funcnvs4  14954  wrdlen2i  14981  wrd2pr2op  14982  wrd3tpop  14987  wwlktovf1  14996  wrdl3s3  15001  relexp1g  15065  dfid6  15067  sgnval  15127  harmonic  15895  prodf1f  15928  fprodntriv  15978  prod1  15980  fprodss  15984  fprodn0f  16027  ege2le3  16126  ruclem8  16273  ruclem11  16276  1nprm  16716  pcmpt  16930  smndex2dnrinv  18928  mgmnsgrpex  18944  pmtrprfval  19505  pmtrprfvalrn  19506  psgnprfval  19539  psgnprfval1  19540  abvtrivd  20833  pzriprng1ALT  21507  cnmsgnsubg  21595  psdmplcl  22166  psdmul  22170  psdmvr  22173  m2detleiblem1  22630  m2detleiblem5  22631  m2detleiblem6  22632  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  imasdsf1olem  24383  pcopt  25055  pcopt2  25056  pcoass  25057  ehl1eudis  25454  ehl2eudis  25456  voliunlem1  25585  i1f1lem  25724  i1f1  25725  itg11  25726  iblcnlem1  25823  bddibl  25875  dvexp  25991  dvef  26018  mvth  26031  iaa  26367  aalioulem2  26375  efrlim  27012  efrlimOLD  27013  amgmlem  27033  amgm  27034  wilthlem2  27112  wilthlem3  27113  basellem7  27130  basellem9  27132  ppiublem2  27247  pclogsum  27259  bposlem5  27332  lgsfval  27346  lgsdir2lem3  27371  lgsdir  27376  lgsdilem2  27377  lgsdi  27378  lgsne0  27379  addsqnreup  27487  ostth1  27677  istrkg2ld  28468  axlowdimlem4  28960  axlowdimlem6  28962  axlowdimlem10  28966  axlowdimlem11  28967  axlowdimlem12  28968  axlowdimlem13  28969  axlowdim1  28974  umgr2v2eedg  29542  umgr2v2e  29543  umgr2v2evd2  29545  2wlklem  29685  usgr2trlncl  29780  2wlkdlem4  29948  2wlkdlem5  29949  2pthdlem1  29950  2wlkdlem10  29955  wwlks2onv  29973  elwwlks2ons3im  29974  umgrwwlks2on  29977  3wlkdlem4  30181  3wlkdlem5  30182  3pthdlem1  30183  3wlkdlem10  30188  upgr3v3e3cycl  30199  upgr4cycl4dv4e  30204  konigsberglem4  30274  konigsberglem5  30275  ex-xp  30455  nmopun  32033  pjnmopi  32167  iuninc  32573  fprodex01  32827  s2rnOLD  32928  s3rnOLD  32930  psgnid  33117  cyc3fv2  33158  cnmsgn0g  33166  cyc3evpm  33170  sgnsval  33181  sgnsf  33182  1fldgenq  33324  constrconj  33786  cntnevol  34229  ddeval1  34235  ddeval0  34236  eulerpartgbij  34374  coinfliprv  34485  sgncl  34541  prodfzo03  34618  circlevma  34657  circlemethhgt  34658  hgt750lemg  34669  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  subfacp1lem1  35184  subfacp1lem2a  35185  subfacp1lem3  35187  subfacp1lem5  35189  cvmliftlem10  35299  sinccvglem  35677  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  itg2addnclem  37678  sticksstones11  42157  readvrec  42392  rabren3dioph  42826  2nn0ind  42957  flcidc  43182  dfrcl4  43689  fvilbdRP  43703  fvrcllb1d  43708  iunrelexp0  43715  corclrcl  43720  relexp1idm  43727  cotrcltrcl  43738  trclfvdecomr  43741  corcltrcl  43752  cotrclrcl  43755  dvsid  44350  binomcxplemnotnn0  44375  refsum2cnlem1  45042  infleinf  45383  itgsin0pilem1  45965  fourierdlem29  46151  fourierdlem56  46177  fourierdlem62  46183  fourierswlem  46245  fouriersw  46246  fun2dmnopgexmpl  47296  sbgoldbo  47774  nnsum3primes4  47775  nnsum3primesgbe  47779  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  cycl3grtrilem  47913  stgr1  47928  usgrexmpl1lem  47980  usgrexmpl1tri  47984  usgrexmpl2lem  47985  usgrexmpl2nb0  47990  usgrexmpl2nb1  47991  usgrexmpl2nb2  47992  usgrexmpl2trifr  47996  gpgedgel  48007  gpgvtx1  48009  opgpgvtx  48010  gpgedgvtx1  48020  gpgvtxedg0  48021  gpgvtxedg1  48022  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  gpg3nbgrvtx0  48032  gpg3nbgrvtx0ALT  48033  gpg3nbgrvtx1  48034  gpgcubic  48035  gpg5nbgr3star  48037  gpg3kgrtriex  48045  zlmodzxzel  48271  zlmodzxz0  48272  zlmodzxzscm  48273  zlmodzxzadd  48274  blenval  48492  nn0sumshdiglemB  48541  fv2arycl  48569  2arympt  48570  2arymptfv  48571  2arymaptf1  48574  2arymaptfo  48575  fv1prop  48620  rrx2pxel  48632  prelrrx2  48634  prelrrx2b  48635  rrx2pnecoorneor  48636  rrx2xpref1o  48639  rrx2plordisom  48644  ehl2eudisval0  48646  rrx2line  48661  rrx2linest  48663  rrx2linesl  48664  2sphere0  48671  line2ylem  48672  line2  48673  line2xlem  48674  line2x  48675  line2y  48676  itscnhlinecirc02p  48706  inlinecirc02plem  48707