Theorem snid 4626

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3453  {csn 4587

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-sn 4588

This theorem is used by:  vsnid  4627  rabsnt  4695  sseliALT  5270  0sn0ep  5563  opthprc  5723  dmsnsnsn  6220  snsn0non  6488  fvrn0  6910  fsn  7133  fsn2  7134  fnsnbOLD  7168  fmptsng  7170  fmptsnd  7171  fvsng  7182  ovima0  7597  brtpos0  8235  tfrlem11  8381  mapsncnv  8904  0elixp  8940  domunsncan  9079  enfixsn  9088  infeq5i  9619  tc2  9723  djulcl  9919  djurcl  9920  djulf1o  9921  djuun  9935  isfin4p1  10321  fin1a2lem12  10417  dcomex  10453  axdc3lem4  10459  zornn0g  10511  axpowndlem3  10612  canthp1lem2  10666  elreal2  11145  xrinfmss  13366  fseq1p1m1  13657  1exp  14159  wrdexb  14594  divalgmod  16502  0bits  16535  lcmfunsnlem2  16736  0ram  17118  setsid  17305  imasvscafn  17629  imasvscaval  17630  gsumval2  18794  0subm  18932  gsumz  18951  smndex1mnd  19028  smndex1id  19029  mulgfval  19198  psgnsn  19653  psgnprfval2  19656  c0snmhm  20610  pzriprnglem4  21703  pzriprnglem5  21704  pzriprnglem7  21706  pzriprnglem9  21708  pzriprnglem13  21712  pzriprnglem14  21713  pzriprng1ALT  21715  mat0dimscm  22697  mat0scmat  22766  mvmumamul1  22782  m1detdiag  22825  pmatcoe1fsupp  22932  d0mat2pmat  22969  pmatcollpw3fi1lem1  23017  pmatcollpw3fi1lem2  23018  chpmat0d  23065  dfac14  23850  filconn  24115  uffix  24153  cnextfvval  24297  cnextcn  24299  ust0  24452  bndth  25192  ehl1eudis  25654  minveclem4a  25664  dvef  26214  tdeglem2  26293  mdegcl  26301  aalioulem2  26576  cxplogb  27031  xrlimcnp  27213  gausslemma2dlem4  27613  cofcutr  28197  cofcutrtime  28200  addsproplem4  28245  addsproplem5  28246  addsproplem6  28247  addsuniflem  28274  negsproplem4  28304  negsproplem5  28305  negsproplem6  28306  mulsproplem12  28400  sltmuls1  28420  sltmuls2  28421  mulsuniflem  28422  precsexlem11  28490  twocut  28696  pw2cut2  28735  axlowdimlem8  29414  axlowdimlem11  29417  upgr1e  29578  uspgr1e  29712  wlkl1loop  30105  wlk1walk  30106  wlk2v2elem1  30643  frgrncvvdeqlem7  30793  hsn0elch  31737  rabsnel  32983  aciunf1lem  33143  gsumwrd2dccatlem  33525  cyc2fv1  33569  1arithidom  33955  ply1dg1rtn0  33999  0mplrim  34032  vieta  34098  lvecdim0  34125  lvecendof1f1o  34151  repr0  35127  bnj97  35383  bnj553  35415  bnj966  35461  bnj1442  35566  fineqvinfep  35659  subfacp1lem2a  35767  subfacp1lem5  35771  cvmliftlem4  35875  fmla0xp  35970  prv1n  36018  bj-0eltag  37730  poimirlem3  38380  poimirlem9  38386  poimirlem31  38408  poimirlem32  38409  prdsbnd  38551  heiborlem3  38571  grposnOLD  38640  grpokerinj  38651  0idl  38783  0rngo  38785  sticksstones11  43030  0prjspnlem  43477  0prjspnrel  43481  fvilbdRP  44538  frege54cor1c  44763  binomcxplemnotnn0  45188  snsslVD  45659  snssl  45660  unipwrVD  45662  unipwr  45663  sucidALTVD  45700  sucidALT  45701  sucidVD  45702  unisnALT  45756  nregmodel  45848  eliuniincex  45949  cnrefiisplem  46665  0cnf  46713  qndenserrnbl  47131  nnfoctbdjlem  47291  isomenndlem  47366  hoidmvlelem2  47432  hoiqssbl  47461  tannpoly  47766  sinnpoly  47767  funressnfv  47939  el1fzopredsuc  48222  setsidel  48284  sbgoldbo  48711  lincval0  49353  lcoel0  49366  1arympt1  49576  discsubc  49998  setc1onsubc  50536  initocmd  50603