Theorem snidg 4660

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {csn 4626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sn 4627

This theorem is referenced by:  snidb  4661  elsn2g  4664  elinsn  4710  snnzg  4774  sneqrg  4839  selsALT  5444  intidg  5462  eldmressnsn  6042  elsnxp  6311  fvressn  7182  fvsnun1  7202  fsnunfv  7207  resf1extb  7956  1stconst  8125  2ndconst  8126  curry1  8129  curry2  8132  suppsnop  8203  mapsnd  8926  en1uniel  9069  dif1enlem  9196  dif1enlemOLD  9197  unifpw  9395  sucprcreg  9641  djurf1o  9953  cfsuc  10297  elfzomin  13776  hashrabsn1  14413  swrds1  14704  fsumsplitsnun  15791  lcmfunsnlem1  16674  ramub1lem1  17064  basprssdmsets  17259  acsfiindd  18598  mgm1  18671  mnd1id  18793  odf1o1  19590  gsumconst  19952  lspsolv  21145  mat1ghm  22489  mat1mhm  22490  mavmul0  22558  m1detdiag  22603  mdetrlin  22608  mdetrsca  22609  chpmat1dlem  22841  maxlp  23155  cnpdis  23301  conncompid  23439  dislly  23505  locfindis  23538  dfac14lem  23625  txtube  23648  pt1hmeo  23814  ufileu  23927  filufint  23928  uffix  23929  uffixsn  23933  i1fima2sn  25715  ply1rem  26205  noextenddif  27713  noextendlt  27714  noextendgt  27715  cutlt  27966  addsval  27995  negsunif  28087  mulsval  28135  mulsproplem5  28146  mulsproplem6  28147  mulsproplem7  28148  mulsproplem8  28149  mulsuniflem  28175  edglnl  29160  vtxd0nedgb  29506  1loopgrvd2  29521  wlkp1  29699  1wlkdlem2  30157  1conngr  30213  frgrwopregasn  30335  frgrwopregbsn  30336  wlkl0  30386  elrspunsn  33457  rtelextdg2  33768  esumel  34048  actfunsnrndisj  34620  reprsuc  34630  breprexplema  34645  derangsn  35175  erdszelem4  35199  cvmlift2lem9  35316  fv1stcnv  35777  fv2ndcnv  35778  neibastop2lem  36361  bj-nsnid  37071  bj-snmoore  37114  ismrer1  37845  elpaddatriN  39805  fnsnbt  42271  frlmsnic  42550  kelac2  43077  rngunsnply  43181  brtrclfv2  43740  k0004lem3  44162  projf1o  45202  fsneq  45211  fsneqrn  45216  unirnmapsn  45219  ssmapsn  45221  fconst7  45271  mccllem  45612  limcresiooub  45657  limcresioolb  45658  cnfdmsn  45897  cxpcncf2  45914  dvmptfprodlem  45959  dvnprodlem1  45961  dvnprodlem2  45962  dvnprodlem3  45963  fourierdlem49  46170  prsal  46333  salexct  46349  salgencntex  46358  sge0sn  46394  sge0snmpt  46398  sge0snmptf  46452  caratheodorylem1  46541  hoiprodp1  46603  hoidmv1le  46609  hoidmvlelem1  46610  hoidmvlelem2  46611  hoidmvlelem3  46612  hoidmvlelem4  46613  hspmbllem2  46642  ovnovollem1  46671  ovnovollem2  46672  funressnfv  47055  cfsetsnfsetf  47070  cfsetsnfsetfo  47072  el1fzopredsuc  47337  snlindsntor  48388  lmod1lem1  48404  lmod1lem2  48405  lmod1lem3  48406  lmod1lem4  48407  lmod1lem5  48408  lmod1zr  48410