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

Theorem 1ex 10626
Description: One is a set. (Contributed by David A. Wheeler, 7-Jul-2016.)
Assertion
Ref Expression
1ex 1 ∈ V

Proof of Theorem 1ex
StepHypRef Expression
1 ax-1cn 10584 . 2 1 ∈ ℂ
21elexi 3460 1 1 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2111  Vcvv 3441  cc 10524  1c1 10527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770  ax-1cn 10584
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443
This theorem is referenced by:  1nn  11636  dfnn2  11638  nn1suc  11647  nn0ind-raph  12070  fzprval  12963  fztpval  12964  expval  13427  m1expcl2  13447  1exp  13454  facnn  13631  fac0  13632  prhash2ex  13756  funcnvs2  14266  funcnvs3  14267  funcnvs4  14268  wrdlen2i  14295  wrd2pr2op  14296  wrd3tpop  14301  wwlktovf1  14312  wrdl3s3  14317  relexp1g  14377  dfid6  14379  sgnval  14439  harmonic  15206  prodf1f  15240  fprodntriv  15288  prod1  15290  fprodss  15294  fprodn0f  15337  ege2le3  15435  ruclem8  15582  ruclem11  15585  1nprm  16013  pcmpt  16218  smndex2dnrinv  18072  mgmnsgrpex  18088  pmtrprfval  18607  pmtrprfvalrn  18608  psgnprfval  18641  psgnprfval1  18642  abvtrivd  19604  cnmsgnsubg  20266  m2detleiblem1  21229  m2detleiblem5  21230  m2detleiblem6  21231  m2detleiblem3  21234  m2detleiblem4  21235  m2detleib  21236  imasdsf1olem  22980  pcopt  23627  pcopt2  23628  pcoass  23629  ehl1eudis  24024  ehl2eudis  24026  voliunlem1  24154  i1f1lem  24293  i1f1  24294  itg11  24295  iblcnlem1  24391  bddibl  24443  dvexp  24556  dvef  24583  mvth  24595  iaa  24921  aalioulem2  24929  efrlim  25555  amgmlem  25575  amgm  25576  wilthlem2  25654  wilthlem3  25655  basellem7  25672  basellem9  25674  ppiublem2  25787  pclogsum  25799  bposlem5  25872  lgsfval  25886  lgsdir2lem3  25911  lgsdir  25916  lgsdilem2  25917  lgsdi  25918  lgsne0  25919  addsqnreup  26027  ostth1  26217  istrkg2ld  26254  axlowdimlem4  26739  axlowdimlem6  26741  axlowdimlem10  26745  axlowdimlem11  26746  axlowdimlem12  26747  axlowdimlem13  26748  axlowdim1  26753  umgr2v2eedg  27314  umgr2v2e  27315  umgr2v2evd2  27317  2wlklem  27457  usgr2trlncl  27549  2wlkdlem4  27714  2wlkdlem5  27715  2pthdlem1  27716  2wlkdlem10  27721  wwlks2onv  27739  elwwlks2ons3im  27740  umgrwwlks2on  27743  3wlkdlem4  27947  3wlkdlem5  27948  3pthdlem1  27949  3wlkdlem10  27954  upgr3v3e3cycl  27965  upgr4cycl4dv4e  27970  konigsberglem4  28040  konigsberglem5  28041  ex-xp  28221  nmopun  29797  pjnmopi  29931  iuninc  30324  fprodex01  30567  s2rn  30646  s3rn  30648  psgnid  30789  cyc3fv2  30830  cnmsgn0g  30838  cyc3evpm  30842  sgnsval  30853  sgnsf  30854  cntnevol  31597  ddeval1  31603  ddeval0  31604  eulerpartgbij  31740  coinfliprv  31850  sgncl  31906  prodfzo03  31984  circlevma  32023  circlemethhgt  32024  hgt750lemg  32035  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  tgoldbachgt  32044  subfacp1lem1  32536  subfacp1lem2a  32537  subfacp1lem3  32539  subfacp1lem5  32541  cvmliftlem10  32651  sinccvglem  33025  poimirlem1  35055  poimirlem2  35056  poimirlem3  35057  poimirlem4  35058  poimirlem6  35060  poimirlem7  35061  poimirlem10  35064  poimirlem11  35065  poimirlem12  35066  poimirlem16  35070  poimirlem17  35071  poimirlem19  35073  poimirlem20  35074  poimirlem23  35077  poimirlem24  35078  poimirlem25  35079  poimirlem28  35082  poimirlem29  35083  poimirlem31  35085  itg2addnclem  35105  rabren3dioph  39751  2nn0ind  39881  flcidc  40113  dfrcl4  40372  fvilbdRP  40386  fvrcllb1d  40391  iunrelexp0  40398  corclrcl  40403  relexp1idm  40410  cotrcltrcl  40421  trclfvdecomr  40424  corcltrcl  40435  cotrclrcl  40438  dvsid  41030  binomcxplemnotnn0  41055  refsum2cnlem1  41661  infleinf  41999  itgsin0pilem1  42587  fourierdlem29  42773  fourierdlem56  42799  fourierdlem62  42805  fourierswlem  42867  fouriersw  42868  fun2dmnopgexmpl  43835  sbgoldbo  44300  nnsum3primes4  44301  nnsum3primesgbe  44305  nnsum4primesodd  44309  nnsum4primesoddALTV  44310  zlmodzxzel  44752  zlmodzxz0  44753  zlmodzxzscm  44754  zlmodzxzadd  44755  blenval  44980  nn0sumshdiglemB  45029  fv2arycl  45057  2arympt  45058  2arymptfv  45059  2arymaptf1  45062  2arymaptfo  45063  fv1prop  45108  rrx2pxel  45120  prelrrx2  45122  prelrrx2b  45123  rrx2pnecoorneor  45124  rrx2xpref1o  45127  rrx2plordisom  45132  ehl2eudisval0  45134  rrx2line  45149  rrx2linest  45151  rrx2linesl  45152  2sphere0  45159  line2ylem  45160  line2  45161  line2xlem  45162  line2x  45163  line2y  45164  itscnhlinecirc02p  45194  inlinecirc02plem  45195
  Copyright terms: Public domain W3C validator