Theorem 1ex 11286

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ℂcc 11182  1c1 11185

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-1cn 11242

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490

This theorem is referenced by:  1nn  12304  dfnn2  12306  nn1suc  12315  nn0ind-raph  12743  fzprval  13645  fztpval  13646  expval  14114  m1expcl2  14136  1exp  14142  facnn  14324  fac0  14325  prhash2ex  14448  funcnvs2  14962  funcnvs3  14963  funcnvs4  14964  wrdlen2i  14991  wrd2pr2op  14992  wrd3tpop  14997  wwlktovf1  15006  wrdl3s3  15011  relexp1g  15075  dfid6  15077  sgnval  15137  harmonic  15907  prodf1f  15940  fprodntriv  15990  prod1  15992  fprodss  15996  fprodn0f  16039  ege2le3  16138  ruclem8  16285  ruclem11  16288  1nprm  16726  pcmpt  16939  smndex2dnrinv  18950  mgmnsgrpex  18966  pmtrprfval  19529  pmtrprfvalrn  19530  psgnprfval  19563  psgnprfval1  19564  abvtrivd  20855  pzriprng1ALT  21530  cnmsgnsubg  21618  psdmplcl  22189  psdmul  22193  m2detleiblem1  22651  m2detleiblem5  22652  m2detleiblem6  22653  m2detleiblem3  22656  m2detleiblem4  22657  m2detleib  22658  imasdsf1olem  24404  pcopt  25074  pcopt2  25075  pcoass  25076  ehl1eudis  25473  ehl2eudis  25475  voliunlem1  25604  i1f1lem  25743  i1f1  25744  itg11  25745  iblcnlem1  25843  bddibl  25895  dvexp  26011  dvef  26038  mvth  26051  iaa  26385  aalioulem2  26393  efrlim  27030  efrlimOLD  27031  amgmlem  27051  amgm  27052  wilthlem2  27130  wilthlem3  27131  basellem7  27148  basellem9  27150  ppiublem2  27265  pclogsum  27277  bposlem5  27350  lgsfval  27364  lgsdir2lem3  27389  lgsdir  27394  lgsdilem2  27395  lgsdi  27396  lgsne0  27397  addsqnreup  27505  ostth1  27695  istrkg2ld  28486  axlowdimlem4  28978  axlowdimlem6  28980  axlowdimlem10  28984  axlowdimlem11  28985  axlowdimlem12  28986  axlowdimlem13  28987  axlowdim1  28992  umgr2v2eedg  29560  umgr2v2e  29561  umgr2v2evd2  29563  2wlklem  29703  usgr2trlncl  29796  2wlkdlem4  29961  2wlkdlem5  29962  2pthdlem1  29963  2wlkdlem10  29968  wwlks2onv  29986  elwwlks2ons3im  29987  umgrwwlks2on  29990  3wlkdlem4  30194  3wlkdlem5  30195  3pthdlem1  30196  3wlkdlem10  30201  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  konigsberglem4  30287  konigsberglem5  30288  ex-xp  30468  nmopun  32046  pjnmopi  32180  iuninc  32583  fprodex01  32829  s2rnOLD  32910  s3rnOLD  32912  psgnid  33090  cyc3fv2  33131  cnmsgn0g  33139  cyc3evpm  33143  sgnsval  33154  sgnsf  33155  1fldgenq  33289  constrconj  33735  cntnevol  34192  ddeval1  34198  ddeval0  34199  eulerpartgbij  34337  coinfliprv  34447  sgncl  34503  prodfzo03  34580  circlevma  34619  circlemethhgt  34620  hgt750lemg  34631  hgt750lemb  34633  hgt750lema  34634  hgt750leme  34635  tgoldbachgtde  34637  tgoldbachgt  34640  subfacp1lem1  35147  subfacp1lem2a  35148  subfacp1lem3  35150  subfacp1lem5  35152  cvmliftlem10  35262  sinccvglem  35640  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem10  37590  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem28  37608  poimirlem29  37609  poimirlem31  37611  itg2addnclem  37631  sticksstones11  42113  rabren3dioph  42771  2nn0ind  42902  flcidc  43131  dfrcl4  43638  fvilbdRP  43652  fvrcllb1d  43657  iunrelexp0  43664  corclrcl  43669  relexp1idm  43676  cotrcltrcl  43687  trclfvdecomr  43690  corcltrcl  43701  cotrclrcl  43704  dvsid  44300  binomcxplemnotnn0  44325  refsum2cnlem1  44937  infleinf  45287  itgsin0pilem1  45871  fourierdlem29  46057  fourierdlem56  46083  fourierdlem62  46089  fourierswlem  46151  fouriersw  46152  fun2dmnopgexmpl  47199  sbgoldbo  47661  nnsum3primes4  47662  nnsum3primesgbe  47666  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  usgrexmpl1lem  47836  usgrexmpl1tri  47840  usgrexmpl2lem  47841  usgrexmpl2nb0  47846  usgrexmpl2nb1  47847  usgrexmpl2nb2  47848  usgrexmpl2trifr  47852  zlmodzxzel  48080  zlmodzxz0  48081  zlmodzxzscm  48082  zlmodzxzadd  48083  blenval  48305  nn0sumshdiglemB  48354  fv2arycl  48382  2arympt  48383  2arymptfv  48384  2arymaptf1  48387  2arymaptfo  48388  fv1prop  48433  rrx2pxel  48445  prelrrx2  48447  prelrrx2b  48448  rrx2pnecoorneor  48449  rrx2xpref1o  48452  rrx2plordisom  48457  ehl2eudisval0  48459  rrx2line  48474  rrx2linest  48476  rrx2linesl  48477  2sphere0  48484  line2ylem  48485  line2  48486  line2xlem  48487  line2x  48488  line2y  48489  itscnhlinecirc02p  48519  inlinecirc02plem  48520