Theorem snidg 4618

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

Syntax hints:   → wi 4   = wceq 1559   ∈ wcel 2141  {csn 4581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4582

This theorem is referenced by:  snidb  4619  elsn2g  4622  elinsn  4668  snnzg  4732  sneqrg  4796  selsALT  5407  intidg  5423  eldmressnsn  6008  elsnxp  6274  fsneq  7012  fvressn  7141  fnsnbg  7144  fvsnun1  7162  fsnunfv  7167  resf1extb  7911  1stconst  8074  2ndconst  8075  curry1  8078  curry2  8081  suppsnop  8153  mapsnd  8864  en1uniel  9006  dif1enlem  9124  unifpw  9295  sucprcregOLD  9552  djurf1o  9868  cfsuc  10211  elfzomin  13740  hashrabsn1  14384  swrds1  14677  fsumsplitsnun  15765  lcmfunsnlem1  16654  ramub1lem1  17045  basprssdmsets  17240  acsfiindd  18568  mgm1  18675  mnd1id  18797  odf1o1  19595  gsumconst  19957  lspsolv  21193  mat1ghm  22523  mat1mhm  22524  mavmul0  22592  m1detdiag  22637  mdetrlin  22642  mdetrsca  22643  chpmat1dlem  22875  maxlp  23187  cnpdis  23333  conncompid  23471  dislly  23537  locfindis  23570  dfac14lem  23657  txtube  23680  pt1hmeo  23846  ufileu  23959  filufint  23960  uffix  23961  uffixsn  23965  i1fima2sn  25722  ply1rem  26206  noextenddif  27709  noextendlt  27710  noextendgt  27711  cutlt  28002  addsval  28032  negsunif  28125  mulsval  28179  mulsproplem5  28190  mulsproplem6  28191  mulsproplem7  28192  mulsproplem8  28193  mulsuniflem  28219  edglnl  29290  vtxd0nedgb  29635  1loopgrvd2  29650  wlkp1  29826  1wlkdlem2  30286  1conngr  30342  frgrwopregasn  30464  frgrwopregbsn  30465  wlkl0  30515  fconst7v  32772  elrspunsn  33576  selvply1rhmlemb  33777  mplmulmvr  33797  esplyind  33833  rtelextdg2  33985  esumel  34305  actfunsnrndisj  34863  reprsuc  34873  breprexplema  34888  derangsn  35484  erdszelem4  35508  cvmlift2lem9  35625  fv1stcnv  36091  fv2ndcnv  36092  neibastop2lem  36684  ttcsnssg  36840  ttcsnidg  36841  bj-nsnid  37519  bj-snmoore  37567  ismrer1  38301  elpaddatriN  40391  frlmsnic  43122  kelac2  43606  rngunsnply  43710  brtrclfv2  44267  k0004lem3  44689  projf1o  45738  fsneqrn  45751  unirnmapsn  45754  ssmapsn  45756  fconst7  45803  mccllem  46137  limcresiooub  46180  limcresioolb  46181  cnfdmsn  46420  cxpcncf2  46437  dvmptfprodlem  46482  dvnprodlem1  46484  dvnprodlem2  46485  dvnprodlem3  46486  fourierdlem49  46693  prsal  46856  salexct  46872  salgencntex  46881  sge0sn  46917  sge0snmpt  46921  sge0snmptf  46975  caratheodorylem1  47064  hoiprodp1  47126  hoidmv1le  47132  hoidmvlelem1  47133  hoidmvlelem2  47134  hoidmvlelem3  47135  hoidmvlelem4  47136  hspmbllem2  47165  ovnovollem1  47194  ovnovollem2  47195  funressnfv  47601  cfsetsnfsetf  47616  cfsetsnfsetfo  47618  el1fzopredsuc  47884  snlindsntor  49057  lmod1lem1  49073  lmod1lem2  49074  lmod1lem3  49075  lmod1lem4  49076  lmod1lem5  49077  lmod1zr  49079  funcsn  50126