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

Step	Hyp	Ref	Expression
1		snid.1	. 2 ⊢ 𝐴 ∈ V
2		snidb 4154	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 219	1 ⊢ 𝐴 ∈ {𝐴}

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  4719  elALT  4837  intid  4853  opthprc  5089  dmsnsnsn  5531  snsn0non  5763  fvrn0  6126  fsn  6308  fsn2  6309  fnsnb  6337  fmptsng  6339  fmptsnd  6340  fvsn  6351  fvsnun1  6353  ovima0  6711  brtpos0  7246  tfrlem11  7371  mapsn  7785  mapsncnv  7790  0elixp  7825  domunsncan  7945  enfixsn  7954  infeq5i  8416  tc2  8501  isfin4-3  9020  fin1a2lem12  9116  dcomex  9152  axdc3lem4  9158  zornn0g  9210  axpowndlem3  9300  canthp1lem2  9354  elreal2  9832  xrinfmss  12012  fseq1p1m1  12283  1exp  12751  wrdexb  13171  divalgmod  14967  0bits  14999  lcmfunsnlem2  15191  0ram  15562  setsid  15742  imasvscafn  16020  imasvscaval  16021  xpsc0  16043  xpsc1  16044  gsumval2  17103  gsumz  17197  psgnsn  17763  psgnprfval2  17766  mat0dimscm  20094  mat0scmat  20163  mvmumamul1  20179  m1detdiag  20222  pmatcoe1fsupp  20325  d0mat2pmat  20362  pmatcollpw3fi1lem1  20410  pmatcollpw3fi1lem2  20411  chpmat0d  20458  dfac14  21231  filcon  21497  uffix  21535  cnextfvval  21679  cnextcn  21681  ust0  21833  bndth  22565  minveclem4a  23009  dvef  23547  tdeglem2  23625  mdegcl  23633  aalioulem2  23892  cxplogb  24324  xrlimcnp  24495  gausslemma2dlem4  24894  axlowdimlem8  25629  axlowdimlem11  25632  uhgrstrrepelem  25744  upgr1e  25779  vdgrf  26425  frgrancvvdeqlem7  26563  frgrancvvdeqlemA  26564  hsn0elch  27489  rabsnel  28726  aciunf1lem  28844  signstfvn  29972  bnj145OLD  30049  bnj97  30190  bnj553  30222  bnj966  30268  bnj1442  30371  subfacp1lem2a  30416  subfacp1lem5  30420  cvmliftlem4  30524  bj-0eltag  32159  poimirlem3  32582  poimirlem9  32588  poimirlem31  32610  poimirlem32  32611  prdsbnd  32762  heiborlem3  32782  grposnOLD  32851  grpokerinj  32862  0idl  32994  0rngo  32996  fvilbdRP  37001  frege54cor1c  37229  binomcxplemnotnn0  37577  snsslVD  38086  snssl  38087  unipwrVD  38089  unipwr  38090  sucidALTVD  38128  sucidALT  38129  sucidVD  38130  unisnALT  38184  eliuniincex  38323  mapsnd  38383  0cnf  38762  dvmptfprod  38835  qndenserrnbl  39191  nnfoctbdjlem  39348  isomenndlem  39420  hoidmvlelem2  39486  hoiqssbl  39515  funressnfv  39857  el1fzopredsuc  39948  uspgr1e  40470  1wlkl1loop  40842  1wlk1walk  40843  1wlk2v2elem1  41322  frgrncvvdeqlem7  41475  frgrncvvdeqlemA  41476  c0snmhm  41705  lincval0  41998  lcoel0  42011