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

Theorem snid 4155
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 4154 . 2 (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
31, 2mpbi 219 1 𝐴 ∈ {𝐴}
Colors of variables: wff setvar class
Syntax hints:  wcel 1977  Vcvv 3173  {csn 4125
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126
This theorem is referenced by:  vsnid  4156  rabsnt  4210  sseliALT  4714  elALT  4832  intid  4847  opthprc  5079  dmsnsnsn  5517  snsn0non  5749  fvrn0  6111  fsn  6293  fsn2  6294  fnsnb  6315  fmptsng  6317  fmptsnd  6318  fvsn  6329  fvsnun1  6331  ovima0  6689  brtpos0  7224  tfrlem11  7349  mapsn  7763  mapsncnv  7768  0elixp  7803  domunsncan  7923  enfixsn  7932  infeq5i  8394  tc2  8479  isfin4-3  8998  fin1a2lem12  9094  dcomex  9130  axdc3lem4  9136  zornn0g  9188  axpowndlem3  9278  canthp1lem2  9332  elreal2  9810  xrinfmss  11971  fseq1p1m1  12241  1exp  12709  wrdexb  13120  divalgmod  14916  0bits  14948  lcmfunsnlem2  15140  0ram  15511  setsid  15691  imasvscafn  15969  imasvscaval  15970  xpsc0  15992  xpsc1  15993  gsumval2  17052  gsumz  17146  psgnsn  17712  psgnprfval2  17715  mat0dimscm  20042  mat0scmat  20111  mvmumamul1  20127  m1detdiag  20170  pmatcoe1fsupp  20273  d0mat2pmat  20310  pmatcollpw3fi1lem1  20358  pmatcollpw3fi1lem2  20359  chpmat0d  20406  dfac14  21179  filcon  21445  uffix  21483  cnextfvval  21627  cnextcn  21629  ust0  21781  bndth  22513  minveclem4a  22954  dvef  23492  tdeglem2  23570  mdegcl  23578  aalioulem2  23837  cxplogb  24269  xrlimcnp  24440  gausslemma2dlem4  24839  axlowdimlem8  25575  axlowdimlem11  25578  vdgrf  26219  frgrancvvdeqlem7  26357  frgrancvvdeqlemA  26358  hsn0elch  27283  rabsnel  28520  aciunf1lem  28638  signstfvn  29766  bnj145OLD  29843  bnj97  29984  bnj553  30016  bnj966  30062  bnj1442  30165  subfacp1lem2a  30210  subfacp1lem5  30214  cvmliftlem4  30318  bj-0eltag  31953  poimirlem3  32376  poimirlem9  32382  poimirlem31  32404  poimirlem32  32405  prdsbnd  32556  heiborlem3  32576  grposnOLD  32645  grpokerinj  32656  0idl  32788  0rngo  32790  fvilbdRP  36795  frege54cor1c  37023  binomcxplemnotnn0  37371  snsslVD  37880  snssl  37881  unipwrVD  37883  unipwr  37884  sucidALTVD  37922  sucidALT  37923  sucidVD  37924  unisnALT  37978  eliuniincex  38117  mapsnd  38177  0cnf  38556  dvmptfprod  38629  qndenserrnbl  38985  nnfoctbdjlem  39142  isomenndlem  39214  hoidmvlelem2  39280  hoiqssbl  39309  funressnfv  39651  el1fzopredsuc  39743  uhgrstrrepelem  40295  upgr1e  40330  uspgr1e  40462  1wlkl1loop  40834  1wlk1walk  40835  1wlk2v2elem1  41314  frgrncvvdeqlem7  41467  frgrncvvdeqlemA  41468  c0snmhm  41697  lincval0  41990  lcoel0  42003
  Copyright terms: Public domain W3C validator