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

Theorem 1ex 11158
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 11116 . 2 1 ∈ ℂ
21elexi 3467 1 1 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3448  cc 11056  1c1 11059
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708  ax-1cn 11116
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450
This theorem is referenced by:  1nn  12171  dfnn2  12173  nn1suc  12182  nn0ind-raph  12610  fzprval  13509  fztpval  13510  expval  13976  m1expcl2  13998  1exp  14004  facnn  14182  fac0  14183  prhash2ex  14306  funcnvs2  14809  funcnvs3  14810  funcnvs4  14811  wrdlen2i  14838  wrd2pr2op  14839  wrd3tpop  14844  wwlktovf1  14853  wrdl3s3  14858  relexp1g  14918  dfid6  14920  sgnval  14980  harmonic  15751  prodf1f  15784  fprodntriv  15832  prod1  15834  fprodss  15838  fprodn0f  15881  ege2le3  15979  ruclem8  16126  ruclem11  16129  1nprm  16562  pcmpt  16771  smndex2dnrinv  18732  mgmnsgrpex  18748  pmtrprfval  19276  pmtrprfvalrn  19277  psgnprfval  19310  psgnprfval1  19311  abvtrivd  20315  cnmsgnsubg  20997  m2detleiblem1  21989  m2detleiblem5  21990  m2detleiblem6  21991  m2detleiblem3  21994  m2detleiblem4  21995  m2detleib  21996  imasdsf1olem  23742  pcopt  24401  pcopt2  24402  pcoass  24403  ehl1eudis  24800  ehl2eudis  24802  voliunlem1  24930  i1f1lem  25069  i1f1  25070  itg11  25071  iblcnlem1  25168  bddibl  25220  dvexp  25333  dvef  25360  mvth  25372  iaa  25701  aalioulem2  25709  efrlim  26335  amgmlem  26355  amgm  26356  wilthlem2  26434  wilthlem3  26435  basellem7  26452  basellem9  26454  ppiublem2  26567  pclogsum  26579  bposlem5  26652  lgsfval  26666  lgsdir2lem3  26691  lgsdir  26696  lgsdilem2  26697  lgsdi  26698  lgsne0  26699  addsqnreup  26807  ostth1  26997  istrkg2ld  27444  axlowdimlem4  27936  axlowdimlem6  27938  axlowdimlem10  27942  axlowdimlem11  27943  axlowdimlem12  27944  axlowdimlem13  27945  axlowdim1  27950  umgr2v2eedg  28514  umgr2v2e  28515  umgr2v2evd2  28517  2wlklem  28657  usgr2trlncl  28750  2wlkdlem4  28915  2wlkdlem5  28916  2pthdlem1  28917  2wlkdlem10  28922  wwlks2onv  28940  elwwlks2ons3im  28941  umgrwwlks2on  28944  3wlkdlem4  29148  3wlkdlem5  29149  3pthdlem1  29150  3wlkdlem10  29155  upgr3v3e3cycl  29166  upgr4cycl4dv4e  29171  konigsberglem4  29241  konigsberglem5  29242  ex-xp  29422  nmopun  30998  pjnmopi  31132  iuninc  31521  fprodex01  31763  s2rn  31842  s3rn  31844  psgnid  31988  cyc3fv2  32029  cnmsgn0g  32037  cyc3evpm  32041  sgnsval  32052  sgnsf  32053  1fldgenq  32129  cntnevol  32867  ddeval1  32873  ddeval0  32874  eulerpartgbij  33012  coinfliprv  33122  sgncl  33178  prodfzo03  33256  circlevma  33295  circlemethhgt  33296  hgt750lemg  33307  hgt750lemb  33309  hgt750lema  33310  hgt750leme  33311  tgoldbachgtde  33313  tgoldbachgt  33316  subfacp1lem1  33813  subfacp1lem2a  33814  subfacp1lem3  33816  subfacp1lem5  33818  cvmliftlem10  33928  sinccvglem  34300  poimirlem1  36108  poimirlem2  36109  poimirlem3  36110  poimirlem4  36111  poimirlem6  36113  poimirlem7  36114  poimirlem10  36117  poimirlem11  36118  poimirlem12  36119  poimirlem16  36123  poimirlem17  36124  poimirlem19  36126  poimirlem20  36127  poimirlem23  36130  poimirlem24  36131  poimirlem25  36132  poimirlem28  36135  poimirlem29  36136  poimirlem31  36138  itg2addnclem  36158  sticksstones11  40593  rabren3dioph  41167  2nn0ind  41298  flcidc  41530  dfrcl4  42022  fvilbdRP  42036  fvrcllb1d  42041  iunrelexp0  42048  corclrcl  42053  relexp1idm  42060  cotrcltrcl  42071  trclfvdecomr  42074  corcltrcl  42085  cotrclrcl  42088  dvsid  42685  binomcxplemnotnn0  42710  refsum2cnlem1  43316  infleinf  43680  itgsin0pilem1  44265  fourierdlem29  44451  fourierdlem56  44477  fourierdlem62  44483  fourierswlem  44545  fouriersw  44546  fun2dmnopgexmpl  45590  sbgoldbo  46053  nnsum3primes4  46054  nnsum3primesgbe  46058  nnsum4primesodd  46062  nnsum4primesoddALTV  46063  zlmodzxzel  46505  zlmodzxz0  46506  zlmodzxzscm  46507  zlmodzxzadd  46508  blenval  46731  nn0sumshdiglemB  46780  fv2arycl  46808  2arympt  46809  2arymptfv  46810  2arymaptf1  46813  2arymaptfo  46814  fv1prop  46859  rrx2pxel  46871  prelrrx2  46873  prelrrx2b  46874  rrx2pnecoorneor  46875  rrx2xpref1o  46878  rrx2plordisom  46883  ehl2eudisval0  46885  rrx2line  46900  rrx2linest  46902  rrx2linesl  46903  2sphere0  46910  line2ylem  46911  line2  46912  line2xlem  46913  line2x  46914  line2y  46915  itscnhlinecirc02p  46945  inlinecirc02plem  46946
  Copyright terms: Public domain W3C validator