Theorem 1ex 11241

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

Syntax hints:   ∈ wcel 2099  Vcvv 3471  ℂcc 11137  1c1 11140

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-1cn 11197

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473

This theorem is referenced by:  1nn  12254  dfnn2  12256  nn1suc  12265  nn0ind-raph  12693  fzprval  13595  fztpval  13596  expval  14061  m1expcl2  14083  1exp  14089  facnn  14267  fac0  14268  prhash2ex  14391  funcnvs2  14897  funcnvs3  14898  funcnvs4  14899  wrdlen2i  14926  wrd2pr2op  14927  wrd3tpop  14932  wwlktovf1  14941  wrdl3s3  14946  relexp1g  15006  dfid6  15008  sgnval  15068  harmonic  15838  prodf1f  15871  fprodntriv  15919  prod1  15921  fprodss  15925  fprodn0f  15968  ege2le3  16067  ruclem8  16214  ruclem11  16217  1nprm  16650  pcmpt  16861  smndex2dnrinv  18867  mgmnsgrpex  18883  pmtrprfval  19442  pmtrprfvalrn  19443  psgnprfval  19476  psgnprfval1  19477  abvtrivd  20720  pzriprng1ALT  21422  cnmsgnsubg  21509  psdmplcl  22086  psdmul  22090  m2detleiblem1  22539  m2detleiblem5  22540  m2detleiblem6  22541  m2detleiblem3  22544  m2detleiblem4  22545  m2detleib  22546  imasdsf1olem  24292  pcopt  24962  pcopt2  24963  pcoass  24964  ehl1eudis  25361  ehl2eudis  25363  voliunlem1  25492  i1f1lem  25631  i1f1  25632  itg11  25633  iblcnlem1  25730  bddibl  25782  dvexp  25898  dvef  25925  mvth  25938  iaa  26273  aalioulem2  26281  efrlim  26914  efrlimOLD  26915  amgmlem  26935  amgm  26936  wilthlem2  27014  wilthlem3  27015  basellem7  27032  basellem9  27034  ppiublem2  27149  pclogsum  27161  bposlem5  27234  lgsfval  27248  lgsdir2lem3  27273  lgsdir  27278  lgsdilem2  27279  lgsdi  27280  lgsne0  27281  addsqnreup  27389  ostth1  27579  istrkg2ld  28277  axlowdimlem4  28769  axlowdimlem6  28771  axlowdimlem10  28775  axlowdimlem11  28776  axlowdimlem12  28777  axlowdimlem13  28778  axlowdim1  28783  umgr2v2eedg  29351  umgr2v2e  29352  umgr2v2evd2  29354  2wlklem  29494  usgr2trlncl  29587  2wlkdlem4  29752  2wlkdlem5  29753  2pthdlem1  29754  2wlkdlem10  29759  wwlks2onv  29777  elwwlks2ons3im  29778  umgrwwlks2on  29781  3wlkdlem4  29985  3wlkdlem5  29986  3pthdlem1  29987  3wlkdlem10  29992  upgr3v3e3cycl  30003  upgr4cycl4dv4e  30008  konigsberglem4  30078  konigsberglem5  30079  ex-xp  30259  nmopun  31837  pjnmopi  31971  iuninc  32364  fprodex01  32601  s2rn  32680  s3rn  32682  psgnid  32831  cyc3fv2  32872  cnmsgn0g  32880  cyc3evpm  32884  sgnsval  32895  sgnsf  32896  1fldgenq  33022  cntnevol  33847  ddeval1  33853  ddeval0  33854  eulerpartgbij  33992  coinfliprv  34102  sgncl  34158  prodfzo03  34235  circlevma  34274  circlemethhgt  34275  hgt750lemg  34286  hgt750lemb  34288  hgt750lema  34289  hgt750leme  34290  tgoldbachgtde  34292  tgoldbachgt  34295  subfacp1lem1  34789  subfacp1lem2a  34790  subfacp1lem3  34792  subfacp1lem5  34794  cvmliftlem10  34904  sinccvglem  35276  poimirlem1  37094  poimirlem2  37095  poimirlem3  37096  poimirlem4  37097  poimirlem6  37099  poimirlem7  37100  poimirlem10  37103  poimirlem11  37104  poimirlem12  37105  poimirlem16  37109  poimirlem17  37110  poimirlem19  37112  poimirlem20  37113  poimirlem23  37116  poimirlem24  37117  poimirlem25  37118  poimirlem28  37121  poimirlem29  37122  poimirlem31  37124  itg2addnclem  37144  sticksstones11  41628  rabren3dioph  42235  2nn0ind  42366  flcidc  42598  dfrcl4  43106  fvilbdRP  43120  fvrcllb1d  43125  iunrelexp0  43132  corclrcl  43137  relexp1idm  43144  cotrcltrcl  43155  trclfvdecomr  43158  corcltrcl  43169  cotrclrcl  43172  dvsid  43768  binomcxplemnotnn0  43793  refsum2cnlem1  44399  infleinf  44754  itgsin0pilem1  45338  fourierdlem29  45524  fourierdlem56  45550  fourierdlem62  45556  fourierswlem  45618  fouriersw  45619  fun2dmnopgexmpl  46664  sbgoldbo  47127  nnsum3primes4  47128  nnsum3primesgbe  47132  nnsum4primesodd  47136  nnsum4primesoddALTV  47137  zlmodzxzel  47419  zlmodzxz0  47420  zlmodzxzscm  47421  zlmodzxzadd  47422  blenval  47644  nn0sumshdiglemB  47693  fv2arycl  47721  2arympt  47722  2arymptfv  47723  2arymaptf1  47726  2arymaptfo  47727  fv1prop  47772  rrx2pxel  47784  prelrrx2  47786  prelrrx2b  47787  rrx2pnecoorneor  47788  rrx2xpref1o  47791  rrx2plordisom  47796  ehl2eudisval0  47798  rrx2line  47813  rrx2linest  47815  rrx2linesl  47816  2sphere0  47823  line2ylem  47824  line2  47825  line2xlem  47826  line2x  47827  line2y  47828  itscnhlinecirc02p  47858  inlinecirc02plem  47859