Theorem snid 4684

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-sn 4649

This theorem is referenced by:  vsnid  4685  rabsnt  4756  sseliALT  5327  intidOLD  5478  0sn0ep  5603  opthprc  5764  dmsnsnsn  6251  snsn0non  6520  fvrn0  6950  fsn  7169  fsn2  7170  fnsnb  7200  fmptsng  7202  fmptsnd  7203  fvsng  7214  ovima0  7629  brtpos0  8274  tfrlem11  8444  mapsncnv  8951  0elixp  8987  domunsncan  9138  enfixsn  9147  infeq5i  9705  tc2  9811  djulcl  9979  djurcl  9980  djulf1o  9981  djuun  9995  isfin4p1  10384  fin1a2lem12  10480  dcomex  10516  axdc3lem4  10522  zornn0g  10574  axpowndlem3  10668  canthp1lem2  10722  elreal2  11201  xrinfmss  13372  fseq1p1m1  13658  1exp  14142  wrdexb  14573  divalgmod  16454  0bits  16485  lcmfunsnlem2  16687  0ram  17067  setsid  17255  imasvscafn  17597  imasvscaval  17598  gsumval2  18724  0subm  18852  gsumz  18871  smndex1mnd  18945  smndex1id  18946  mulgfval  19109  psgnsn  19562  psgnprfval2  19565  c0snmhm  20489  pzriprnglem4  21518  pzriprnglem5  21519  pzriprnglem7  21521  pzriprnglem9  21523  pzriprnglem13  21527  pzriprnglem14  21528  pzriprng1ALT  21530  mat0dimscm  22496  mat0scmat  22565  mvmumamul1  22581  m1detdiag  22624  pmatcoe1fsupp  22728  d0mat2pmat  22765  pmatcollpw3fi1lem1  22813  pmatcollpw3fi1lem2  22814  chpmat0d  22861  dfac14  23647  filconn  23912  uffix  23950  cnextfvval  24094  cnextcn  24096  ust0  24249  bndth  25009  ehl1eudis  25473  minveclem4a  25483  dvef  26038  tdeglem2  26120  mdegcl  26128  aalioulem2  26393  cxplogb  26847  xrlimcnp  27029  gausslemma2dlem4  27431  cofcutr  27976  cofcutrtime  27979  addsproplem4  28023  addsproplem5  28024  addsproplem6  28025  addsuniflem  28052  negsproplem4  28081  negsproplem5  28082  negsproplem6  28083  mulsproplem12  28171  ssltmul1  28191  ssltmul2  28192  mulsuniflem  28193  precsexlem11  28259  axlowdimlem8  28982  axlowdimlem11  28985  upgr1e  29148  uspgr1e  29279  wlkl1loop  29674  wlk1walk  29675  wlk2v2elem1  30187  frgrncvvdeqlem7  30337  hsn0elch  31280  rabsnel  32528  aciunf1lem  32680  cyc2fv1  33114  1arithidom  33530  ply1dg1rtn0  33570  lvecdim0  33619  lvecendof1f1o  33646  repr0  34588  bnj97  34842  bnj553  34874  bnj966  34920  bnj1442  35025  subfacp1lem2a  35148  subfacp1lem5  35152  cvmliftlem4  35256  fmla0xp  35351  prv1n  35399  bj-0eltag  36944  poimirlem3  37583  poimirlem9  37589  poimirlem31  37611  poimirlem32  37612  prdsbnd  37753  heiborlem3  37773  grposnOLD  37842  grpokerinj  37853  0idl  37985  0rngo  37987  sticksstones11  42113  0prjspnlem  42578  0prjspnrel  42582  fvilbdRP  43652  frege54cor1c  43877  binomcxplemnotnn0  44325  snsslVD  44800  snssl  44801  unipwrVD  44803  unipwr  44804  sucidALTVD  44841  sucidALT  44842  sucidVD  44843  unisnALT  44897  eliuniincex  45011  cnrefiisplem  45750  0cnf  45798  dvmptfprod  45866  qndenserrnbl  46216  nnfoctbdjlem  46376  isomenndlem  46451  hoidmvlelem2  46517  hoiqssbl  46546  funressnfv  46958  el1fzopredsuc  47240  setsidel  47250  sbgoldbo  47661  lincval0  48144  lcoel0  48157  1arympt1  48372