Theorem snidg 4055

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 28-Oct-2003.)

Assertion

Ref	Expression
snidg

Proof of Theorem snidg

Step	Hyp	Ref	Expression
1		eqid 2457	. 2
2		elsncg 4052	. 2
3	1, 2	mpbiri 233	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  {csn 4029

This theorem is referenced by:  snidb  4056  elsnc2g  4059  snnzg  4147  eldmressnsn  5318  fvressn  6087  fsnunfv  6111  1stconst  6888  2ndconst  6889  curry1  6892  curry2  6895  suppsnop  6932  en1uniel  7607  unifpw  7843  sucprcreg  8046  mapfienOLD  8159  cfsuc  8658  elfzomin  11887  hashrabsn1  12442  eqs1  12621  swrds1  12676  ramub1lem1  14544  acsfiindd  15807  mgm1  15884  mnd1OLD  15962  mnd1id  15963  odf1o1  16592  gsumconst  16954  lspsolv  17789  mat1ghm  18985  mat1mhm  18986  mavmul0  19054  m1detdiag  19099  mdetrlin  19104  mdetrsca  19105  chpmat1dlem  19336  maxlp  19648  cnpdis  19794  concompid  19932  dislly  19998  locfindis  20031  dfac14lem  20118  txtube  20141  pt1hmeo  20307  ufileu  20420  filufint  20421  uffix  20422  uffixsn  20426  i1fima2sn  22087  ply1rem  22564  1conngra  24675  vdgr1d  24903  vdgr1a  24906  eupap1  24976  esumel  28058  derangsn  28614  erdszelem4  28638  cvmlift2lem9  28756  neibastop2lem  30178  ismrer1  30334  kelac2  31011  rngunsnply  31122  mccllem  31605  limcresiooub  31648  limcresioolb  31649  cnfdmsn  31684  cxpcncf2  31703  dvmptfprodlem  31741  dvnprodlem1  31743  dvnprodlem2  31744  dvnprodlem3  31745  fourierdlem49  31938  funressnfv  32213  snlindsntor  33072  lmod1lem1  33088  lmod1lem2  33089  lmod1lem3  33090  lmod1lem4  33091  lmod1lem5  33092  lmod1zr  33094  bj-sels  34520  elpaddatriN  35527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030