Theorem snid 4623

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 4622	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 233	1 ⊢ 𝐴 ∈ {𝐴}

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-sn 4589

This theorem is used by:  vsnid  4624  rabsnt  4692  sseliALT  5267  0sn0ep  5560  opthprc  5720  dmsnsnsn  6235  snsn0non  6510  fvrn0  6939  fsn  7163  fsn2  7164  fmptsng  7199  fmptsnd  7200  fvsng  7211  ovima0  7627  brtpos0  8281  tfrlem11  8427  mapsncnv  8952  0elixp  8988  domunsncan  9127  enfixsn  9136  infeq5i  9667  tc2  9771  djulcl  10021  djurcl  10022  djulf1o  10023  djuun  10037  isfin4p1  10423  fin1a2lem12  10519  dcomex  10555  axdc3lem4  10561  zornn0g  10613  axpowndlem3  10714  canthp1lem2  10768  elreal2  11247  xrinfmss  13470  fseq1p1m1  13762  1exp  14264  wrdexb  14700  divalgmod  16608  0bits  16641  lcmfunsnlem2  16847  0ram  17230  setsid  17417  imasvscafn  17741  imasvscaval  17742  gsumval2  18907  0subm  19045  gsumz  19064  smndex1mnd  19141  smndex1id  19142  mulgfval  19311  psgnsn  19767  psgnprfval2  19770  c0snmhm  20726  pzriprnglem4  21823  pzriprnglem5  21824  pzriprnglem7  21826  pzriprnglem9  21828  pzriprnglem13  21832  pzriprnglem14  21833  pzriprng1ALT  21835  mat0dimscm  22817  mat0scmat  22886  mvmumamul1  22902  m1detdiag  22945  pmatcoe1fsupp  23052  d0mat2pmat  23089  pmatcollpw3fi1lem1  23137  pmatcollpw3fi1lem2  23138  chpmat0d  23185  dfac14  23970  filconn  24235  uffix  24273  cnextfvval  24417  cnextcn  24419  ust0  24572  bndth  25312  ehl1eudis  25774  minveclem4a  25784  dvef  26333  tdeglem2  26412  mdegcl  26420  aalioulem2  26693  cxplogb  27147  xrlimcnp  27329  gausslemma2dlem4  27729  cofcutr  28343  cofcutrtime  28346  addsproplem4  28391  addsproplem5  28392  addsproplem6  28393  addsuniflem  28420  negsproplem4  28450  negsproplem5  28451  negsproplem6  28452  mulsproplem12  28546  sltmuls1  28566  sltmuls2  28567  mulsuniflem  28568  precsexlem11  28636  twocut  28842  pw2cut2  28881  axlowdimlem8  29560  axlowdimlem11  29563  upgr1e  29724  uspgr1e  29858  wlkl1loop  30251  wlk1walk  30252  wlk2v2elem1  30789  frgrncvvdeqlem7  30939  hsn0elch  31883  rabsnel  33171  aciunf1lem  33331  gsumwrd2dccatlem  33714  cyc2fv1  33758  1arithidom  34153  ply1dg1rtn0  34196  0mplrim  34229  vieta  34295  lvecdim0  34322  lvecendof1f1o  34348  repr0  35323  bnj97  35579  bnj553  35611  bnj966  35657  bnj1442  35762  fineqvinfep  35906  subfacp1lem2a  36125  subfacp1lem5  36129  cvmliftlem4  36233  fmla0xp  36328  prv1n  36376  bj-0eltag  38082  poimirlem3  38746  poimirlem9  38752  poimirlem31  38774  poimirlem32  38775  prdsbnd  38930  heiborlem3  38950  grposnOLD  39019  grpokerinj  39030  0idl  39162  0rngo  39164  sticksstones11  43409  0prjspnlem  43866  0prjspnrel  43867  fvilbdRP  44893  frege54cor1c  45118  binomcxplemnotnn0  45543  snsslVD  46013  snssl  46014  unipwrVD  46016  unipwr  46017  sucidALTVD  46054  sucidALT  46055  sucidVD  46056  unisnALT  46110  nregmodel  46213  eliuniincex  46339  cnrefiisplem  47054  0cnf  47102  qndenserrnbl  47520  nnfoctbdjlem  47680  isomenndlem  47755  hoidmvlelem2  47821  hoiqssbl  47850  tannpoly  48155  sinnpoly  48156  funressnfv  48328  el1fzopredsuc  48611  setsidel  48673  sbgoldbo  49100  lincval0  49742  lcoel0  49755  1arympt1  49965  discsubc  50393  setc1onsubc  50955  parhomid2  50966  parhomid  50967  parcatid2  50978  parcatid  50979  initocmd  51067