Theorem 1ex 11119

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ℂcc 11015  1c1 11018

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-1cn 11075

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439

This theorem is referenced by:  1nn  12147  dfnn2  12149  nn1suc  12158  nn0ind-raph  12583  fzprval  13492  fztpval  13493  expval  13977  m1expcl2  13999  1exp  14005  facnn  14189  fac0  14190  prhash2ex  14313  funcnvs2  14827  funcnvs3  14828  funcnvs4  14829  wrdlen2i  14856  wrd2pr2op  14857  wrd3tpop  14862  wwlktovf1  14871  wrdl3s3  14876  relexp1g  14940  dfid6  14942  sgnval  15002  harmonic  15773  prodf1f  15806  fprodntriv  15856  prod1  15858  fprodss  15862  fprodn0f  15905  ege2le3  16004  ruclem8  16153  ruclem11  16156  1nprm  16597  pcmpt  16811  smndex2dnrinv  18831  mgmnsgrpex  18847  pmtrprfval  19407  pmtrprfvalrn  19408  psgnprfval  19441  psgnprfval1  19442  abvtrivd  20756  pzriprng1ALT  21442  cnmsgnsubg  21523  psdmplcl  22096  psdmul  22100  psdmvr  22103  m2detleiblem1  22559  m2detleiblem5  22560  m2detleiblem6  22561  m2detleiblem3  22564  m2detleiblem4  22565  m2detleib  22566  imasdsf1olem  24308  pcopt  24969  pcopt2  24970  pcoass  24971  ehl1eudis  25367  ehl2eudis  25369  voliunlem1  25498  i1f1lem  25637  i1f1  25638  itg11  25639  iblcnlem1  25736  bddibl  25788  dvexp  25904  dvef  25931  mvth  25944  iaa  26280  aalioulem2  26288  efrlim  26926  efrlimOLD  26927  amgmlem  26947  amgm  26948  wilthlem2  27026  wilthlem3  27027  basellem7  27044  basellem9  27046  ppiublem2  27161  pclogsum  27173  bposlem5  27246  lgsfval  27260  lgsdir2lem3  27285  lgsdir  27290  lgsdilem2  27291  lgsdi  27292  lgsne0  27293  addsqnreup  27401  ostth1  27591  istrkg2ld  28458  axlowdimlem4  28944  axlowdimlem6  28946  axlowdimlem10  28950  axlowdimlem11  28951  axlowdimlem12  28952  axlowdimlem13  28953  axlowdim1  28958  umgr2v2eedg  29524  umgr2v2e  29525  umgr2v2evd2  29527  2wlklem  29665  usgr2trlncl  29759  2wlkdlem4  29927  2wlkdlem5  29928  2pthdlem1  29929  2wlkdlem10  29934  wwlks2onv  29952  elwwlks2ons3im  29953  usgrwwlks2on  29957  umgrwwlks2on  29958  3wlkdlem4  30163  3wlkdlem5  30164  3pthdlem1  30165  3wlkdlem10  30170  upgr3v3e3cycl  30181  upgr4cycl4dv4e  30186  konigsberglem4  30256  konigsberglem5  30257  ex-xp  30437  nmopun  32015  pjnmopi  32149  iuninc  32561  fprodex01  32834  sgncl  32840  s2rnOLD  32954  s3rnOLD  32956  psgnid  33107  cyc3fv2  33148  cnmsgn0g  33156  cyc3evpm  33160  sgnsval  33171  sgnsf  33172  1fldgenq  33332  gsumind  33354  constrconj  33830  nn0constr  33846  cntnevol  34313  ddeval1  34319  ddeval0  34320  eulerpartgbij  34457  coinfliprv  34568  prodfzo03  34688  circlevma  34727  circlemethhgt  34728  hgt750lemg  34739  hgt750lemb  34741  hgt750lema  34742  hgt750leme  34743  tgoldbachgtde  34745  tgoldbachgt  34748  subfacp1lem1  35295  subfacp1lem2a  35296  subfacp1lem3  35298  subfacp1lem5  35300  cvmliftlem10  35410  sinccvglem  35788  poimirlem1  37734  poimirlem2  37735  poimirlem3  37736  poimirlem4  37737  poimirlem6  37739  poimirlem7  37740  poimirlem10  37743  poimirlem11  37744  poimirlem12  37745  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem28  37761  poimirlem29  37762  poimirlem31  37764  itg2addnclem  37784  sticksstones11  42322  readvrec  42532  rabren3dioph  42972  2nn0ind  43102  flcidc  43327  dfrcl4  43833  fvilbdRP  43847  fvrcllb1d  43852  iunrelexp0  43859  corclrcl  43864  relexp1idm  43871  cotrcltrcl  43882  trclfvdecomr  43885  corcltrcl  43896  cotrclrcl  43899  dvsid  44488  binomcxplemnotnn0  44513  refsum2cnlem1  45198  infleinf  45532  itgsin0pilem1  46110  fourierdlem29  46296  fourierdlem56  46322  fourierdlem62  46328  fourierswlem  46390  fouriersw  46391  nthrucw  47046  lamberte  47050  cjnpoly  47051  fun2dmnopgexmpl  47446  sbgoldbo  47949  nnsum3primes4  47950  nnsum3primesgbe  47954  nnsum4primesodd  47958  nnsum4primesoddALTV  47959  cycl3grtrilem  48108  stgr1  48123  usgrexmpl1lem  48183  usgrexmpl1tri  48187  usgrexmpl2lem  48188  usgrexmpl2nb0  48193  usgrexmpl2nb1  48194  usgrexmpl2nb2  48195  usgrexmpl2trifr  48199  gpgiedgdmellem  48208  gpgvtx1  48216  opgpgvtx  48217  gpgedgvtx1  48224  gpgvtxedg0  48225  gpgvtxedg1  48226  gpgedgiov  48227  gpgedg2iv  48229  gpg5nbgrvtx03starlem1  48230  gpg5nbgrvtx03starlem3  48232  gpg5nbgrvtx13starlem1  48233  gpg5nbgrvtx13starlem2  48234  gpg5nbgrvtx13starlem3  48235  gpg3nbgrvtx0  48238  gpg3nbgrvtx0ALT  48239  gpg3nbgrvtx1  48240  gpgcubic  48241  gpg5nbgr3star  48243  gpg3kgrtriex  48251  gpgprismgr4cycllem2  48258  gpgprismgr4cycllem3  48259  gpgprismgr4cycllem7  48263  gpgprismgr4cycllem9  48265  pgnioedg1  48270  pgnioedg2  48271  pgnioedg3  48272  pgnioedg4  48273  pgnioedg5  48274  pgnbgreunbgrlem2lem1  48276  pgnbgreunbgrlem2lem2  48277  pgnbgreunbgrlem2lem3  48278  pgnbgreunbgrlem2  48279  pgnbgreunbgrlem3  48280  pgnbgreunbgrlem4  48281  pgnbgreunbgrlem5lem1  48282  pgnbgreunbgrlem5lem2  48283  pgnbgreunbgrlem5lem3  48284  pgnbgreunbgrlem6  48286  gpg5edgnedg  48292  grlimedgnedg  48293  zlmodzxzel  48517  zlmodzxz0  48518  zlmodzxzscm  48519  zlmodzxzadd  48520  blenval  48733  nn0sumshdiglemB  48782  fv2arycl  48810  2arympt  48811  2arymptfv  48812  2arymaptf1  48815  2arymaptfo  48816  fv1prop  48861  rrx2pxel  48873  prelrrx2  48875  prelrrx2b  48876  rrx2pnecoorneor  48877  rrx2xpref1o  48880  rrx2plordisom  48885  ehl2eudisval0  48887  rrx2line  48902  rrx2linest  48904  rrx2linesl  48905  2sphere0  48912  line2ylem  48913  line2  48914  line2xlem  48915  line2x  48916  line2y  48917  itscnhlinecirc02p  48947  inlinecirc02plem  48948