MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  1ex Structured version   Visualization version   GIF version

Theorem 1ex 9891
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
StepHypRef Expression
1 ax-1cn 9850 . 2 1 ∈ ℂ
21elexi 3185 1 1 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1976  Vcvv 3172  cc 9790  1c1 9793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-12 2033  ax-ext 2589  ax-1cn 9850
This theorem depends on definitions:  df-bi 195  df-an 384  df-tru 1477  df-ex 1695  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-v 3174
This theorem is referenced by:  1nn  10878  dfnn2  10880  nn1suc  10888  nn0ind-raph  11309  fzprval  12226  fztpval  12227  expval  12679  m1expcl2  12699  1exp  12706  facnn  12879  fac0  12880  prhash2ex  13000  funcnvs2  13454  funcnvs3  13455  funcnvs4  13456  wrdlen2i  13480  wrd2pr2op  13481  wrd3tpop  13485  wwlktovf1  13494  wrdl3s3  13499  relexp1g  13560  dfid6  13562  sgnval  13622  harmonic  14376  prodf1f  14409  fprodntriv  14457  prod1  14459  fprodss  14463  fprodn0f  14507  ege2le3  14605  ruclem8  14751  ruclem11  14754  1nprm  15176  isprm2lem  15178  pcmpt  15380  mgmnsgrpex  17187  pmtrprfval  17676  pmtrprfvalrn  17677  psgnprfval  17710  psgnprfval1  17711  abvtrivd  18609  cnmsgnsubg  19687  m2detleiblem1  20191  m2detleiblem5  20192  m2detleiblem6  20193  m2detleiblem3  20196  m2detleiblem4  20197  m2detleib  20198  imasdsf1olem  21929  pcopt  22561  pcopt2  22562  pcoass  22563  voliunlem1  23042  i1f1lem  23179  i1f1  23180  itg11  23181  iblcnlem1  23277  bddibl  23329  dvexp  23439  mvth  23476  iaa  23801  aalioulem2  23809  efrlim  24413  amgmlem  24433  amgm  24434  wilthlem2  24512  wilthlem3  24513  basellem7  24530  basellem9  24532  ppiublem2  24645  pclogsum  24657  bposlem5  24730  lgsfval  24744  lgsdir2lem3  24769  lgsdir  24774  lgsdilem2  24775  lgsdi  24776  lgsne0  24777  ostth1  25039  istrkg2ld  25076  axlowdimlem4  25543  axlowdimlem6  25545  axlowdimlem10  25549  axlowdimlem11  25550  axlowdimlem12  25551  axlowdimlem13  25552  axlowdim1  25557  2trllemH  25848  2trllemE  25849  2wlklemB  25851  wlkntrllem1  25855  wlkntrllem2  25856  wlkntrllem3  25857  2wlklem  25860  constr1trl  25884  1pthon  25887  2pthlem1  25891  2pthlem2  25892  2wlklem1  25893  usgra2wlkspthlem1  25913  usgra2wlkspthlem2  25914  constr3lem2  25940  constr3lem4  25941  constr3lem5  25942  constr3trllem1  25944  constr3trllem2  25945  el2wlkonotlem  26155  usg2wlkonot  26176  usg2wotspth  26177  ex-xp  26451  nmopun  28063  pjnmopi  28197  iuninc  28567  sgnsval  28865  sgnsf  28866  psgnid  28984  cntnevol  29424  ddeval1  29430  ddeval0  29431  eulerpartgbij  29567  coinfliprv  29677  sgncl  29733  subfacp1lem1  30221  subfacp1lem2a  30222  subfacp1lem3  30224  subfacp1lem5  30226  cvmliftlem10  30336  sinccvglem  30626  poimirlem1  32376  poimirlem2  32377  poimirlem3  32378  poimirlem4  32379  poimirlem6  32381  poimirlem7  32382  poimirlem10  32385  poimirlem11  32386  poimirlem12  32387  poimirlem16  32391  poimirlem17  32392  poimirlem19  32394  poimirlem20  32395  poimirlem23  32398  poimirlem24  32399  poimirlem25  32400  poimirlem28  32403  poimirlem29  32404  poimirlem31  32406  itg2addnclem  32427  rabren3dioph  36193  2nn0ind  36324  flcidc  36559  dfrcl4  36783  fvilbdRP  36797  fvrcllb1d  36802  iunrelexp0  36809  corclrcl  36814  relexp1idm  36821  cotrcltrcl  36832  trclfvdecomr  36835  corcltrcl  36846  cotrclrcl  36849  dvsid  37348  binomcxplemnotnn0  37373  refsum2cnlem1  38015  infleinf  38326  itgsin0pilem1  38638  fourierdlem29  38826  fourierdlem56  38852  fourierdlem62  38858  fourierswlem  38920  fouriersw  38921  nnsum3primes4  40002  nnsum3primesgbe  40006  nnsum4primesodd  40010  nnsum4primesoddALTV  40011  fun2dmnopgexmpl  40149  umgr2v2eedg  40735  umgr2v2e  40736  umgr2v2evd2  40738  2Wlklem  40870  usgr2wlkneq  40957  usgr2trlncl  40961  21wlkdlem4  41130  21wlkdlem5  41131  2pthdlem1  41132  21wlkdlem10  41137  wwlks2onv  41153  elwwlks2ons3  41154  umgrwwlks2on  41156  31wlkdlem4  41324  31wlkdlem5  41325  3pthdlem1  41326  31wlkdlem10  41331  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  konigsberglem4  41420  konigsberglem5  41421  zlmodzxzel  41921  zlmodzxz0  41922  zlmodzxzscm  41923  zlmodzxzadd  41924  blenval  42158  nn0sumshdiglemB  42207
  Copyright terms: Public domain W3C validator