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

Theorem 1ex 10073
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 10032 . 2 1 ∈ ℂ
21elexi 3244 1 1 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2030  Vcvv 3231  cc 9972  1c1 9975
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-12 2087  ax-ext 2631  ax-1cn 10032
This theorem depends on definitions:  df-bi 197  df-an 385  df-tru 1526  df-ex 1745  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-v 3233
This theorem is referenced by:  1nn  11069  dfnn2  11071  nn1suc  11079  nn0ind-raph  11515  fzprval  12439  fztpval  12440  expval  12902  m1expcl2  12922  1exp  12929  facnn  13102  fac0  13103  prhash2ex  13225  funcnvs2  13704  funcnvs3  13705  funcnvs4  13706  wrdlen2i  13732  wrd2pr2op  13733  wrd3tpop  13737  wwlktovf1  13746  wrdl3s3  13751  relexp1g  13810  dfid6  13812  sgnval  13872  harmonic  14635  prodf1f  14668  fprodntriv  14716  prod1  14718  fprodss  14722  fprodn0f  14766  ege2le3  14864  ruclem8  15010  ruclem11  15013  1nprm  15439  pcmpt  15643  mgmnsgrpex  17465  pmtrprfval  17953  pmtrprfvalrn  17954  psgnprfval  17987  psgnprfval1  17988  abvtrivd  18888  cnmsgnsubg  19971  m2detleiblem1  20478  m2detleiblem5  20479  m2detleiblem6  20480  m2detleiblem3  20483  m2detleiblem4  20484  m2detleib  20485  imasdsf1olem  22225  pcopt  22868  pcopt2  22869  pcoass  22870  voliunlem1  23364  i1f1lem  23501  i1f1  23502  itg11  23503  iblcnlem1  23599  bddibl  23651  dvexp  23761  mvth  23800  iaa  24125  aalioulem2  24133  efrlim  24741  amgmlem  24761  amgm  24762  wilthlem2  24840  wilthlem3  24841  basellem7  24858  basellem9  24860  ppiublem2  24973  pclogsum  24985  bposlem5  25058  lgsfval  25072  lgsdir2lem3  25097  lgsdir  25102  lgsdilem2  25103  lgsdi  25104  lgsne0  25105  ostth1  25367  istrkg2ld  25404  axlowdimlem4  25870  axlowdimlem6  25872  axlowdimlem10  25876  axlowdimlem11  25877  axlowdimlem12  25878  axlowdimlem13  25879  axlowdim1  25884  umgr2v2eedg  26476  umgr2v2e  26477  umgr2v2evd2  26479  2wlklem  26619  usgr2trlncl  26712  2wlkdlem4  26893  2wlkdlem5  26894  2pthdlem1  26895  2wlkdlem10  26900  wwlks2onv  26918  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  3wlkdlem4  27140  3wlkdlem5  27141  3pthdlem1  27142  3wlkdlem10  27147  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  konigsberglem4  27233  konigsberglem5  27234  2clwwlk2clwwlklem2lem2  27329  ex-xp  27423  nmopun  29001  pjnmopi  29135  iuninc  29505  fprodex01  29699  sgnsval  29856  sgnsf  29857  psgnid  29975  cntnevol  30419  ddeval1  30425  ddeval0  30426  eulerpartgbij  30562  coinfliprv  30672  sgncl  30728  prodfzo03  30809  circlevma  30848  circlemethhgt  30849  hgt750lemg  30860  hgt750lemb  30862  hgt750lema  30863  hgt750leme  30864  tgoldbachgtde  30866  tgoldbachgt  30869  subfacp1lem1  31287  subfacp1lem2a  31288  subfacp1lem3  31290  subfacp1lem5  31292  cvmliftlem10  31402  sinccvglem  31692  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  itg2addnclem  33591  rabren3dioph  37696  2nn0ind  37827  flcidc  38061  dfrcl4  38285  fvilbdRP  38299  fvrcllb1d  38304  iunrelexp0  38311  corclrcl  38316  relexp1idm  38323  cotrcltrcl  38334  trclfvdecomr  38337  corcltrcl  38348  cotrclrcl  38351  dvsid  38847  binomcxplemnotnn0  38872  refsum2cnlem1  39510  infleinf  39901  itgsin0pilem1  40483  fourierdlem29  40671  fourierdlem56  40697  fourierdlem62  40703  fourierswlem  40765  fouriersw  40766  fun2dmnopgexmpl  41626  sbgoldbo  42000  nnsum3primes4  42001  nnsum3primesgbe  42005  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  zlmodzxzel  42458  zlmodzxz0  42459  zlmodzxzscm  42460  zlmodzxzadd  42461  blenval  42690  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator