Theorem snidg 4617

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4581

This theorem is referenced by:  snidb  4618  elsn2g  4621  elinsn  4667  snnzg  4731  sneqrg  4795  selsALT  5389  intidg  5405  eldmressnsn  5983  elsnxp  6249  fvressn  7107  fnsnbg  7110  fvsnun1  7128  fsnunfv  7133  resf1extb  7876  1stconst  8042  2ndconst  8043  curry1  8046  curry2  8049  suppsnop  8120  mapsnd  8824  en1uniel  8966  dif1enlem  9084  unifpw  9255  sucprcreg  9509  djurf1o  9825  cfsuc  10167  elfzomin  13653  hashrabsn1  14297  swrds1  14590  fsumsplitsnun  15678  lcmfunsnlem1  16564  ramub1lem1  16954  basprssdmsets  17148  acsfiindd  18476  mgm1  18583  mnd1id  18705  odf1o1  19501  gsumconst  19863  lspsolv  21098  mat1ghm  22427  mat1mhm  22428  mavmul0  22496  m1detdiag  22541  mdetrlin  22546  mdetrsca  22547  chpmat1dlem  22779  maxlp  23091  cnpdis  23237  conncompid  23375  dislly  23441  locfindis  23474  dfac14lem  23561  txtube  23584  pt1hmeo  23750  ufileu  23863  filufint  23864  uffix  23865  uffixsn  23869  i1fima2sn  25637  ply1rem  26127  noextenddif  27636  noextendlt  27637  noextendgt  27638  cutlt  27928  addsval  27958  negsunif  28051  mulsval  28105  mulsproplem5  28116  mulsproplem6  28117  mulsproplem7  28118  mulsproplem8  28119  mulsuniflem  28145  edglnl  29216  vtxd0nedgb  29562  1loopgrvd2  29577  wlkp1  29753  1wlkdlem2  30213  1conngr  30269  frgrwopregasn  30391  frgrwopregbsn  30392  wlkl0  30442  fconst7v  32698  elrspunsn  33510  mplmulmvr  33704  esplyind  33731  rtelextdg2  33884  esumel  34204  actfunsnrndisj  34762  reprsuc  34772  breprexplema  34787  derangsn  35364  erdszelem4  35388  cvmlift2lem9  35505  fv1stcnv  35971  fv2ndcnv  35972  neibastop2lem  36554  bj-nsnid  37271  bj-snmoore  37314  ismrer1  38035  elpaddatriN  40059  frlmsnic  42791  kelac2  43303  rngunsnply  43407  brtrclfv2  43964  k0004lem3  44386  projf1o  45437  fsneq  45446  fsneqrn  45451  unirnmapsn  45454  ssmapsn  45456  fconst7  45504  mccllem  45839  limcresiooub  45882  limcresioolb  45883  cnfdmsn  46122  cxpcncf2  46139  dvmptfprodlem  46184  dvnprodlem1  46186  dvnprodlem2  46187  dvnprodlem3  46188  fourierdlem49  46395  prsal  46558  salexct  46574  salgencntex  46583  sge0sn  46619  sge0snmpt  46623  sge0snmptf  46677  caratheodorylem1  46766  hoiprodp1  46828  hoidmv1le  46834  hoidmvlelem1  46835  hoidmvlelem2  46836  hoidmvlelem3  46837  hoidmvlelem4  46838  hspmbllem2  46867  ovnovollem1  46896  ovnovollem2  46897  funressnfv  47285  cfsetsnfsetf  47300  cfsetsnfsetfo  47302  el1fzopredsuc  47567  snlindsntor  48713  lmod1lem1  48729  lmod1lem2  48730  lmod1lem3  48731  lmod1lem4  48732  lmod1lem5  48733  lmod1zr  48735  funcsn  49782