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

Theorem snid 4564
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)
Hypothesis
Ref Expression
snid.1 𝐴 ∈ V
Assertion
Ref Expression
snid 𝐴 ∈ {𝐴}

Proof of Theorem snid
StepHypRef Expression
1 snid.1 . 2 𝐴 ∈ V
2 snidb 4563 . 2 (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
31, 2mpbi 233 1 𝐴 ∈ {𝐴}
Colors of variables: wff setvar class
Syntax hints:  wcel 2112  Vcvv 3444  {csn 4528
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 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-sn 4529
This theorem is referenced by:  vsnid  4565  rabsnt  4630  sseliALT  5180  elALT  5303  intid  5318  0sn0ep  5438  opthprc  5584  dmsnsnsn  6048  snsn0non  6281  fvrn0  6677  fsn  6878  fsn2  6879  fnsnb  6909  fmptsng  6911  fmptsnd  6912  fvsng  6923  ovima0  7311  brtpos0  7886  tfrlem11  8011  mapsncnv  8444  0elixp  8480  domunsncan  8604  enfixsn  8613  infeq5i  9087  tc2  9172  djulcl  9327  djurcl  9328  djulf1o  9329  djuun  9343  isfin4p1  9730  fin1a2lem12  9826  dcomex  9862  axdc3lem4  9868  zornn0g  9920  axpowndlem3  10014  canthp1lem2  10068  elreal2  10547  xrinfmss  12695  fseq1p1m1  12980  1exp  13458  wrdexb  13872  divalgmod  15751  0bits  15782  lcmfunsnlem2  15978  0ram  16350  setsid  16534  imasvscafn  16806  imasvscaval  16807  gsumval2  17892  0subm  17978  gsumz  17996  smndex1mnd  18071  smndex1id  18072  mulgfval  18222  psgnsn  18644  psgnprfval2  18647  mat0dimscm  21078  mat0scmat  21147  mvmumamul1  21163  m1detdiag  21206  pmatcoe1fsupp  21310  d0mat2pmat  21347  pmatcollpw3fi1lem1  21395  pmatcollpw3fi1lem2  21396  chpmat0d  21443  dfac14  22227  filconn  22492  uffix  22530  cnextfvval  22674  cnextcn  22676  ust0  22829  bndth  23567  ehl1eudis  24028  minveclem4a  24038  dvef  24587  tdeglem2  24666  mdegcl  24674  aalioulem2  24933  cxplogb  25376  xrlimcnp  25558  gausslemma2dlem4  25957  axlowdimlem8  26747  axlowdimlem11  26750  upgr1e  26910  uspgr1e  27038  wlkl1loop  27431  wlk1walk  27432  wlk2v2elem1  27944  frgrncvvdeqlem7  28094  hsn0elch  29035  rabsnel  30274  aciunf1lem  30429  cyc2fv1  30817  lvecdim0  31097  repr0  31996  bnj97  32252  bnj553  32284  bnj966  32330  bnj1442  32435  subfacp1lem2a  32541  subfacp1lem5  32545  cvmliftlem4  32649  fmla0xp  32744  prv1n  32792  bj-0eltag  34415  poimirlem3  35059  poimirlem9  35065  poimirlem31  35087  poimirlem32  35088  prdsbnd  35230  heiborlem3  35250  grposnOLD  35319  grpokerinj  35330  0idl  35462  0rngo  35464  0prjspnlem  39605  0prjspnrel  39606  fvilbdRP  40384  frege54cor1c  40609  binomcxplemnotnn0  41053  snsslVD  41528  snssl  41529  unipwrVD  41531  unipwr  41532  sucidALTVD  41569  sucidALT  41570  sucidVD  41571  unisnALT  41625  eliuniincex  41738  cnrefiisplem  42464  0cnf  42512  dvmptfprod  42580  qndenserrnbl  42930  nnfoctbdjlem  43087  isomenndlem  43162  hoidmvlelem2  43228  hoiqssbl  43257  funressnfv  43628  el1fzopredsuc  43875  setsidel  43886  sbgoldbo  44298  c0snmhm  44532  lincval0  44817  lcoel0  44830  1arympt1  45045
  Copyright terms: Public domain W3C validator