Theorem snidg 4595

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2106  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sn 4562

This theorem is referenced by:  snidb  4596  elsn2g  4599  elinsn  4646  snnzg  4710  sneqrg  4770  sels  5356  eldmressnsn  5934  elsnxp  6194  fvressn  7034  fvsnun1  7054  fsnunfv  7059  1stconst  7940  2ndconst  7941  curry1  7944  curry2  7947  suppsnop  7994  mapsnd  8674  en1uniel  8818  en1unielOLD  8819  dif1enlem  8943  unifpw  9122  sucprcreg  9360  djurf1o  9671  cfsuc  10013  elfzomin  13459  hashrabsn1  14089  swrds1  14379  fsumsplitsnun  15467  lcmfunsnlem1  16342  ramub1lem1  16727  basprssdmsets  16925  acsfiindd  18271  mgm1  18342  mnd1id  18427  odf1o1  19177  gsumconst  19535  lspsolv  20405  mat1ghm  21632  mat1mhm  21633  mavmul0  21701  m1detdiag  21746  mdetrlin  21751  mdetrsca  21752  chpmat1dlem  21984  maxlp  22298  cnpdis  22444  conncompid  22582  dislly  22648  locfindis  22681  dfac14lem  22768  txtube  22791  pt1hmeo  22957  ufileu  23070  filufint  23071  uffix  23072  uffixsn  23076  i1fima2sn  24844  ply1rem  25328  edglnl  27513  vtxd0nedgb  27855  1loopgrvd2  27870  wlkp1  28049  1wlkdlem2  28502  1conngr  28558  frgrwopregasn  28680  frgrwopregbsn  28681  wlkl0  28731  esumel  32015  actfunsnrndisj  32585  reprsuc  32595  breprexplema  32610  derangsn  33132  erdszelem4  33156  cvmlift2lem9  33273  fv1stcnv  33751  fv2ndcnv  33752  noextenddif  33871  noextendlt  33872  noextendgt  33873  addsval  34126  neibastop2lem  34549  bj-nsnid  35241  bj-snmoore  35284  ismrer1  35996  elpaddatriN  37817  fnsnbt  40208  frlmsnic  40263  kelac2  40890  rngunsnply  40998  brtrclfv2  41335  k0004lem3  41759  projf1o  42736  fsneq  42746  fsneqrn  42751  unirnmapsn  42754  ssmapsn  42756  fconst7  42812  mccllem  43138  limcresiooub  43183  limcresioolb  43184  cnfdmsn  43423  cxpcncf2  43440  dvmptfprodlem  43485  dvnprodlem1  43487  dvnprodlem2  43488  dvnprodlem3  43489  fourierdlem49  43696  prsal  43859  salexct  43873  salgencntex  43882  sge0sn  43917  sge0snmpt  43921  sge0snmptf  43975  caratheodorylem1  44064  hoiprodp1  44126  hoidmv1le  44132  hoidmvlelem1  44133  hoidmvlelem2  44134  hoidmvlelem3  44135  hoidmvlelem4  44136  hspmbllem2  44165  ovnovollem1  44194  ovnovollem2  44195  funressnfv  44537  cfsetsnfsetf  44552  cfsetsnfsetfo  44554  el1fzopredsuc  44817  snlindsntor  45812  lmod1lem1  45828  lmod1lem2  45829  lmod1lem3  45830  lmod1lem4  45831  lmod1lem5  45832  lmod1zr  45834