Theorem 1ex 10035

Description: 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)

Assertion

Ref	Expression
1ex	|- 1 e. _V

Proof of Theorem 1ex

Step	Hyp	Ref	Expression
1		ax-1cn 9994	. 2 |- 1 e. CC
2	1	elexi 3213	1 |- 1 e. _V

Syntax hints:   e. wcel 1990   _Vcvv 3200   CCcc 9934   1c1 9937

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-12 2047  ax-ext 2602  ax-1cn 9994

This theorem depends on definitions:  df-bi 197  df-an 386  df-tru 1486  df-ex 1705  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-v 3202

This theorem is referenced by:  1nn  11031  dfnn2  11033  nn1suc  11041  nn0ind-raph  11477  fzprval  12401  fztpval  12402  expval  12862  m1expcl2  12882  1exp  12889  facnn  13062  fac0  13063  prhash2ex  13187  funcnvs2  13658  funcnvs3  13659  funcnvs4  13660  wrdlen2i  13686  wrd2pr2op  13687  wrd3tpop  13691  wwlktovf1  13700  wrdl3s3  13705  relexp1g  13766  dfid6  13768  sgnval  13828  harmonic  14591  prodf1f  14624  fprodntriv  14672  prod1  14674  fprodss  14678  fprodn0f  14722  ege2le3  14820  ruclem8  14966  ruclem11  14969  1nprm  15392  pcmpt  15596  mgmnsgrpex  17418  pmtrprfval  17907  pmtrprfvalrn  17908  psgnprfval  17941  psgnprfval1  17942  abvtrivd  18840  cnmsgnsubg  19923  m2detleiblem1  20430  m2detleiblem5  20431  m2detleiblem6  20432  m2detleiblem3  20435  m2detleiblem4  20436  m2detleib  20437  imasdsf1olem  22178  pcopt  22822  pcopt2  22823  pcoass  22824  voliunlem1  23318  i1f1lem  23456  i1f1  23457  itg11  23458  iblcnlem1  23554  bddibl  23606  dvexp  23716  mvth  23755  iaa  24080  aalioulem2  24088  efrlim  24696  amgmlem  24716  amgm  24717  wilthlem2  24795  wilthlem3  24796  basellem7  24813  basellem9  24815  ppiublem2  24928  pclogsum  24940  bposlem5  25013  lgsfval  25027  lgsdir2lem3  25052  lgsdir  25057  lgsdilem2  25058  lgsdi  25059  lgsne0  25060  ostth1  25322  istrkg2ld  25359  axlowdimlem4  25825  axlowdimlem6  25827  axlowdimlem10  25831  axlowdimlem11  25832  axlowdimlem12  25833  axlowdimlem13  25834  axlowdim1  25839  umgr2v2eedg  26420  umgr2v2e  26421  umgr2v2evd2  26423  2wlklem  26563  usgr2trlncl  26656  2wlkdlem4  26824  2wlkdlem5  26825  2pthdlem1  26826  2wlkdlem10  26831  wwlks2onv  26847  elwwlks2ons3  26848  umgrwwlks2on  26850  3wlkdlem4  27022  3wlkdlem5  27023  3pthdlem1  27024  3wlkdlem10  27029  upgr3v3e3cycl  27040  upgr4cycl4dv4e  27045  konigsberglem4  27117  konigsberglem5  27118  ex-xp  27293  nmopun  28873  pjnmopi  29007  iuninc  29379  fprodex01  29571  sgnsval  29728  sgnsf  29729  psgnid  29847  cntnevol  30291  ddeval1  30297  ddeval0  30298  eulerpartgbij  30434  coinfliprv  30544  sgncl  30600  prodfzo03  30681  circlevma  30720  circlemethhgt  30721  hgt750lemg  30732  hgt750lemb  30734  hgt750lema  30735  hgt750leme  30736  tgoldbachgtde  30738  tgoldbachgt  30741  subfacp1lem1  31161  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem5  31166  cvmliftlem10  31276  sinccvglem  31566  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem10  33419  poimirlem11  33420  poimirlem12  33421  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem28  33437  poimirlem29  33438  poimirlem31  33440  itg2addnclem  33461  rabren3dioph  37379  2nn0ind  37510  flcidc  37744  dfrcl4  37968  fvilbdRP  37982  fvrcllb1d  37987  iunrelexp0  37994  corclrcl  37999  relexp1idm  38006  cotrcltrcl  38017  trclfvdecomr  38020  corcltrcl  38031  cotrclrcl  38034  dvsid  38530  binomcxplemnotnn0  38555  refsum2cnlem1  39196  infleinf  39588  itgsin0pilem1  40165  fourierdlem29  40353  fourierdlem56  40379  fourierdlem62  40385  fourierswlem  40447  fouriersw  40448  fun2dmnopgexmpl  41303  sbgoldbo  41675  nnsum3primes4  41676  nnsum3primesgbe  41680  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  zlmodzxzel  42133  zlmodzxz0  42134  zlmodzxzscm  42135  zlmodzxzadd  42136  blenval  42365  nn0sumshdiglemB  42414