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

Theorem snid 4241
 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 4240 . 2 (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
31, 2mpbi 220 1 𝐴 ∈ {𝐴}
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2030  Vcvv 3231  {csn 4210 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-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sn 4211 This theorem is referenced by:  vsnid  4242  rabsnt  4298  sseliALT  4824  elALT  4940  intid  4956  opthprc  5201  dmsnsnsn  5649  snsn0non  5884  fvrn0  6254  fsn  6442  fsn2  6443  fnsnb  6473  fmptsng  6475  fmptsnd  6476  fvsn  6487  fvsnun1  6489  ovima0  6855  brtpos0  7404  tfrlem11  7529  mapsn  7941  mapsncnv  7946  0elixp  7981  domunsncan  8101  enfixsn  8110  infeq5i  8571  tc2  8656  isfin4-3  9175  fin1a2lem12  9271  dcomex  9307  axdc3lem4  9313  zornn0g  9365  axpowndlem3  9459  canthp1lem2  9513  elreal2  9991  xrinfmss  12178  fseq1p1m1  12452  1exp  12929  wrdexb  13348  divalgmod  15176  0bits  15208  lcmfunsnlem2  15400  0ram  15771  setsid  15961  imasvscafn  16244  imasvscaval  16245  xpsc0  16267  xpsc1  16268  gsumval2  17327  gsumz  17421  psgnsn  17986  psgnprfval2  17989  mat0dimscm  20323  mat0scmat  20392  mvmumamul1  20408  m1detdiag  20451  pmatcoe1fsupp  20554  d0mat2pmat  20591  pmatcollpw3fi1lem1  20639  pmatcollpw3fi1lem2  20640  chpmat0d  20687  dfac14  21469  filconn  21734  uffix  21772  cnextfvval  21916  cnextcn  21918  ust0  22070  bndth  22804  minveclem4a  23247  dvef  23788  tdeglem2  23866  mdegcl  23874  aalioulem2  24133  cxplogb  24569  xrlimcnp  24740  gausslemma2dlem4  25139  axlowdimlem8  25874  axlowdimlem11  25877  upgr1e  26053  uspgr1e  26181  wlkl1loop  26590  wlk1walk  26591  wlk2v2elem1  27133  frgrncvvdeqlem7  27285  hsn0elch  28233  rabsnel  29467  aciunf1lem  29590  signstfvn  30774  repr0  30817  bnj97  31062  bnj553  31094  bnj966  31140  bnj1442  31243  subfacp1lem2a  31288  subfacp1lem5  31292  cvmliftlem4  31396  bj-0eltag  33091  poimirlem3  33542  poimirlem9  33548  poimirlem31  33570  poimirlem32  33571  prdsbnd  33722  heiborlem3  33742  grposnOLD  33811  grpokerinj  33822  0idl  33954  0rngo  33956  fvilbdRP  38299  frege54cor1c  38526  binomcxplemnotnn0  38872  snsslVD  39378  snssl  39379  unipwrVD  39381  unipwr  39382  sucidALTVD  39420  sucidALT  39421  sucidVD  39422  unisnALT  39476  eliuniincex  39606  mapsnd  39702  cnrefiisplem  40373  0cnf  40408  dvmptfprod  40478  qndenserrnbl  40833  nnfoctbdjlem  40990  isomenndlem  41065  hoidmvlelem2  41131  hoiqssbl  41160  funressnfv  41529  el1fzopredsuc  41660  setsidel  41671  sbgoldbo  42000  c0snmhm  42240  lincval0  42529  lcoel0  42542
 Copyright terms: Public domain W3C validator