Theorem 1ex 10794

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

Syntax hints:   ∈ wcel 2112  Vcvv 3398  ℂcc 10692  1c1 10695

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708  ax-1cn 10752

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400

This theorem is referenced by:  1nn  11806  dfnn2  11808  nn1suc  11817  nn0ind-raph  12242  fzprval  13138  fztpval  13139  expval  13602  m1expcl2  13622  1exp  13629  facnn  13806  fac0  13807  prhash2ex  13931  funcnvs2  14443  funcnvs3  14444  funcnvs4  14445  wrdlen2i  14472  wrd2pr2op  14473  wrd3tpop  14478  wwlktovf1  14489  wrdl3s3  14494  relexp1g  14554  dfid6  14556  sgnval  14616  harmonic  15386  prodf1f  15419  fprodntriv  15467  prod1  15469  fprodss  15473  fprodn0f  15516  ege2le3  15614  ruclem8  15761  ruclem11  15764  1nprm  16199  pcmpt  16408  smndex2dnrinv  18296  mgmnsgrpex  18312  pmtrprfval  18833  pmtrprfvalrn  18834  psgnprfval  18867  psgnprfval1  18868  abvtrivd  19830  cnmsgnsubg  20493  m2detleiblem1  21475  m2detleiblem5  21476  m2detleiblem6  21477  m2detleiblem3  21480  m2detleiblem4  21481  m2detleib  21482  imasdsf1olem  23225  pcopt  23873  pcopt2  23874  pcoass  23875  ehl1eudis  24271  ehl2eudis  24273  voliunlem1  24401  i1f1lem  24540  i1f1  24541  itg11  24542  iblcnlem1  24639  bddibl  24691  dvexp  24804  dvef  24831  mvth  24843  iaa  25172  aalioulem2  25180  efrlim  25806  amgmlem  25826  amgm  25827  wilthlem2  25905  wilthlem3  25906  basellem7  25923  basellem9  25925  ppiublem2  26038  pclogsum  26050  bposlem5  26123  lgsfval  26137  lgsdir2lem3  26162  lgsdir  26167  lgsdilem2  26168  lgsdi  26169  lgsne0  26170  addsqnreup  26278  ostth1  26468  istrkg2ld  26505  axlowdimlem4  26990  axlowdimlem6  26992  axlowdimlem10  26996  axlowdimlem11  26997  axlowdimlem12  26998  axlowdimlem13  26999  axlowdim1  27004  umgr2v2eedg  27566  umgr2v2e  27567  umgr2v2evd2  27569  2wlklem  27709  usgr2trlncl  27801  2wlkdlem4  27966  2wlkdlem5  27967  2pthdlem1  27968  2wlkdlem10  27973  wwlks2onv  27991  elwwlks2ons3im  27992  umgrwwlks2on  27995  3wlkdlem4  28199  3wlkdlem5  28200  3pthdlem1  28201  3wlkdlem10  28206  upgr3v3e3cycl  28217  upgr4cycl4dv4e  28222  konigsberglem4  28292  konigsberglem5  28293  ex-xp  28473  nmopun  30049  pjnmopi  30183  iuninc  30573  fprodex01  30813  s2rn  30892  s3rn  30894  psgnid  31037  cyc3fv2  31078  cnmsgn0g  31086  cyc3evpm  31090  sgnsval  31101  sgnsf  31102  cntnevol  31862  ddeval1  31868  ddeval0  31869  eulerpartgbij  32005  coinfliprv  32115  sgncl  32171  prodfzo03  32249  circlevma  32288  circlemethhgt  32289  hgt750lemg  32300  hgt750lemb  32302  hgt750lema  32303  hgt750leme  32304  tgoldbachgtde  32306  tgoldbachgt  32309  subfacp1lem1  32808  subfacp1lem2a  32809  subfacp1lem3  32811  subfacp1lem5  32813  cvmliftlem10  32923  sinccvglem  33297  poimirlem1  35464  poimirlem2  35465  poimirlem3  35466  poimirlem4  35467  poimirlem6  35469  poimirlem7  35470  poimirlem10  35473  poimirlem11  35474  poimirlem12  35475  poimirlem16  35479  poimirlem17  35480  poimirlem19  35482  poimirlem20  35483  poimirlem23  35486  poimirlem24  35487  poimirlem25  35488  poimirlem28  35491  poimirlem29  35492  poimirlem31  35494  itg2addnclem  35514  sticksstones11  39781  rabren3dioph  40281  2nn0ind  40411  flcidc  40643  dfrcl4  40902  fvilbdRP  40916  fvrcllb1d  40921  iunrelexp0  40928  corclrcl  40933  relexp1idm  40940  cotrcltrcl  40951  trclfvdecomr  40954  corcltrcl  40965  cotrclrcl  40968  dvsid  41563  binomcxplemnotnn0  41588  refsum2cnlem1  42194  infleinf  42525  itgsin0pilem1  43109  fourierdlem29  43295  fourierdlem56  43321  fourierdlem62  43327  fourierswlem  43389  fouriersw  43390  fun2dmnopgexmpl  44391  sbgoldbo  44855  nnsum3primes4  44856  nnsum3primesgbe  44860  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  zlmodzxzel  45307  zlmodzxz0  45308  zlmodzxzscm  45309  zlmodzxzadd  45310  blenval  45533  nn0sumshdiglemB  45582  fv2arycl  45610  2arympt  45611  2arymptfv  45612  2arymaptf1  45615  2arymaptfo  45616  fv1prop  45661  rrx2pxel  45673  prelrrx2  45675  prelrrx2b  45676  rrx2pnecoorneor  45677  rrx2xpref1o  45680  rrx2plordisom  45685  ehl2eudisval0  45687  rrx2line  45702  rrx2linest  45704  rrx2linesl  45705  2sphere0  45712  line2ylem  45713  line2  45714  line2xlem  45715  line2x  45716  line2y  45717  itscnhlinecirc02p  45747  inlinecirc02plem  45748