Theorem 1ex 9914

Description: 1 is a set. Common special case. (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 9873	. 2 ⊢ 1 ∈ ℂ
2	1	elexi 3186	1 ⊢ 1 ∈ V

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ℂcc 9813  1c1 9816

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-12 2034  ax-ext 2590  ax-1cn 9873

This theorem depends on definitions:  df-bi 196  df-an 385  df-tru 1478  df-ex 1696  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-v 3175

This theorem is referenced by:  1nn  10908  dfnn2  10910  nn1suc  10918  nn0ind-raph  11353  fzprval  12271  fztpval  12272  expval  12724  m1expcl2  12744  1exp  12751  facnn  12924  fac0  12925  prhash2ex  13048  funcnvs2  13508  funcnvs3  13509  funcnvs4  13510  wrdlen2i  13534  wrd2pr2op  13535  wrd3tpop  13539  wwlktovf1  13548  wrdl3s3  13553  relexp1g  13614  dfid6  13616  sgnval  13676  harmonic  14430  prodf1f  14463  fprodntriv  14511  prod1  14513  fprodss  14517  fprodn0f  14561  ege2le3  14659  ruclem8  14805  ruclem11  14808  1nprm  15230  isprm2lem  15232  pcmpt  15434  mgmnsgrpex  17241  pmtrprfval  17730  pmtrprfvalrn  17731  psgnprfval  17764  psgnprfval1  17765  abvtrivd  18663  cnmsgnsubg  19742  m2detleiblem1  20249  m2detleiblem5  20250  m2detleiblem6  20251  m2detleiblem3  20254  m2detleiblem4  20255  m2detleib  20256  imasdsf1olem  21988  pcopt  22630  pcopt2  22631  pcoass  22632  voliunlem1  23125  i1f1lem  23262  i1f1  23263  itg11  23264  iblcnlem1  23360  bddibl  23412  dvexp  23522  mvth  23559  iaa  23884  aalioulem2  23892  efrlim  24496  amgmlem  24516  amgm  24517  wilthlem2  24595  wilthlem3  24596  basellem7  24613  basellem9  24615  ppiublem2  24728  pclogsum  24740  bposlem5  24813  lgsfval  24827  lgsdir2lem3  24852  lgsdir  24857  lgsdilem2  24858  lgsdi  24859  lgsne0  24860  ostth1  25122  istrkg2ld  25159  axlowdimlem4  25625  axlowdimlem6  25627  axlowdimlem10  25631  axlowdimlem11  25632  axlowdimlem12  25633  axlowdimlem13  25634  axlowdim1  25639  2trllemH  26082  2trllemE  26083  2wlklemB  26085  wlkntrllem1  26089  wlkntrllem2  26090  wlkntrllem3  26091  2wlklem  26094  constr1trl  26118  1pthon  26121  2pthlem1  26125  2pthlem2  26126  2wlklem1  26127  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  constr3lem2  26174  constr3lem4  26175  constr3lem5  26176  constr3trllem1  26178  constr3trllem2  26179  el2wlkonotlem  26389  usg2wlkonot  26410  usg2wotspth  26411  ex-xp  26685  nmopun  28257  pjnmopi  28391  iuninc  28761  sgnsval  29059  sgnsf  29060  psgnid  29178  cntnevol  29618  ddeval1  29624  ddeval0  29625  eulerpartgbij  29761  coinfliprv  29871  sgncl  29927  subfacp1lem1  30415  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem5  30420  cvmliftlem10  30530  sinccvglem  30820  poimirlem1  32580  poimirlem2  32581  poimirlem3  32582  poimirlem4  32583  poimirlem6  32585  poimirlem7  32586  poimirlem10  32589  poimirlem11  32590  poimirlem12  32591  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem23  32602  poimirlem24  32603  poimirlem25  32604  poimirlem28  32607  poimirlem29  32608  poimirlem31  32610  itg2addnclem  32631  rabren3dioph  36397  2nn0ind  36528  flcidc  36763  dfrcl4  36987  fvilbdRP  37001  fvrcllb1d  37006  iunrelexp0  37013  corclrcl  37018  relexp1idm  37025  cotrcltrcl  37036  trclfvdecomr  37039  corcltrcl  37050  cotrclrcl  37053  dvsid  37552  binomcxplemnotnn0  37577  refsum2cnlem1  38219  infleinf  38529  itgsin0pilem1  38841  fourierdlem29  39029  fourierdlem56  39055  fourierdlem62  39061  fourierswlem  39123  fouriersw  39124  nnsum3primes4  40204  nnsum3primesgbe  40208  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  fun2dmnopgexmpl  40329  umgr2v2eedg  40740  umgr2v2e  40741  umgr2v2evd2  40743  2Wlklem  40875  usgr2wlkneq  40962  usgr2trlncl  40966  21wlkdlem4  41135  21wlkdlem5  41136  2pthdlem1  41137  21wlkdlem10  41142  wwlks2onv  41158  elwwlks2ons3  41159  umgrwwlks2on  41161  31wlkdlem4  41329  31wlkdlem5  41330  3pthdlem1  41331  31wlkdlem10  41336  upgr3v3e3cycl  41347  upgr4cycl4dv4e  41352  konigsberglem4  41425  konigsberglem5  41426  zlmodzxzel  41926  zlmodzxz0  41927  zlmodzxzscm  41928  zlmodzxzadd  41929  blenval  42163  nn0sumshdiglemB  42212