Theorem snidg 4604

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 2736	. 2 ⊢ 𝐴 = 𝐴
2		elsng 4581	. 2 ⊢ (𝐴 ∈ 𝑉 → (𝐴 ∈ {𝐴} ↔ 𝐴 = 𝐴))
3	1, 2	mpbiri 258	1 ⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ {𝐴})

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4568

This theorem is referenced by:  snidb  4605  elsn2g  4608  elinsn  4654  snnzg  4718  sneqrg  4782  selsALT  5393  intidg  5409  eldmressnsn  5989  elsnxp  6255  fvressn  7116  fnsnbg  7119  fvsnun1  7137  fsnunfv  7142  resf1extb  7885  1stconst  8050  2ndconst  8051  curry1  8054  curry2  8057  suppsnop  8128  mapsnd  8834  en1uniel  8976  dif1enlem  9094  unifpw  9265  sucprcregOLD  9521  djurf1o  9837  cfsuc  10179  elfzomin  13692  hashrabsn1  14336  swrds1  14629  fsumsplitsnun  15717  lcmfunsnlem1  16606  ramub1lem1  16997  basprssdmsets  17191  acsfiindd  18519  mgm1  18626  mnd1id  18748  odf1o1  19547  gsumconst  19909  lspsolv  21141  mat1ghm  22448  mat1mhm  22449  mavmul0  22517  m1detdiag  22562  mdetrlin  22567  mdetrsca  22568  chpmat1dlem  22800  maxlp  23112  cnpdis  23258  conncompid  23396  dislly  23462  locfindis  23495  dfac14lem  23582  txtube  23605  pt1hmeo  23771  ufileu  23884  filufint  23885  uffix  23886  uffixsn  23890  i1fima2sn  25647  ply1rem  26131  noextenddif  27632  noextendlt  27633  noextendgt  27634  cutlt  27924  addsval  27954  negsunif  28047  mulsval  28101  mulsproplem5  28112  mulsproplem6  28113  mulsproplem7  28114  mulsproplem8  28115  mulsuniflem  28141  edglnl  29212  vtxd0nedgb  29557  1loopgrvd2  29572  wlkp1  29748  1wlkdlem2  30208  1conngr  30264  frgrwopregasn  30386  frgrwopregbsn  30387  wlkl0  30437  fconst7v  32693  elrspunsn  33489  mplmulmvr  33683  esplyind  33719  rtelextdg2  33871  esumel  34191  actfunsnrndisj  34749  reprsuc  34759  breprexplema  34774  derangsn  35352  erdszelem4  35376  cvmlift2lem9  35493  fv1stcnv  35959  fv2ndcnv  35960  neibastop2lem  36542  ttcsnssg  36698  ttcsnidg  36699  bj-nsnid  37377  bj-snmoore  37425  ismrer1  38159  elpaddatriN  40249  frlmsnic  42985  kelac2  43493  rngunsnply  43597  brtrclfv2  44154  k0004lem3  44576  projf1o  45626  fsneq  45635  fsneqrn  45640  unirnmapsn  45643  ssmapsn  45645  fconst7  45693  mccllem  46027  limcresiooub  46070  limcresioolb  46071  cnfdmsn  46310  cxpcncf2  46327  dvmptfprodlem  46372  dvnprodlem1  46374  dvnprodlem2  46375  dvnprodlem3  46376  fourierdlem49  46583  prsal  46746  salexct  46762  salgencntex  46771  sge0sn  46807  sge0snmpt  46811  sge0snmptf  46865  caratheodorylem1  46954  hoiprodp1  47016  hoidmv1le  47022  hoidmvlelem1  47023  hoidmvlelem2  47024  hoidmvlelem3  47025  hoidmvlelem4  47026  hspmbllem2  47055  ovnovollem1  47084  ovnovollem2  47085  funressnfv  47491  cfsetsnfsetf  47506  cfsetsnfsetfo  47508  el1fzopredsuc  47774  snlindsntor  48947  lmod1lem1  48963  lmod1lem2  48964  lmod1lem3  48965  lmod1lem4  48966  lmod1lem5  48967  lmod1zr  48969  funcsn  50016