Theorem snidg 4624

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4588

This theorem is used by:  snidb  4625  elsn2g  4628  elinsn  4674  snnzg  4738  sneqrg  4802  selsALT  5420  intidg  5436  eldmressnsn  6021  elsnxp  6293  fsneq  7031  fvressn  7163  fnsnbg  7166  fvsnun1  7184  fsnunfv  7189  resf1extb  7935  1stconst  8101  2ndconst  8102  curry1  8105  curry2  8108  suppsnop  8180  mapsnd  8897  en1uniel  9040  dif1enlem  9158  unifpw  9326  sucprcregOLD  9583  djurf1o  9922  cfsuc  10263  elfzomin  13797  hashrabsn1  14442  swrds1  14740  fsumsplitsnun  15845  lcmfunsnlem1  16733  ramub1lem1  17124  basprssdmsets  17319  acsfiindd  18647  mgm1  18756  mnd1id  18893  odf1o1  19705  gsumconst  20067  lspsolv  21336  mat1ghm  22711  mat1mhm  22712  mavmul0  22780  m1detdiag  22825  mdetrlin  22830  mdetrsca  22831  chpmat1dlem  23066  maxlp  23378  cnpdis  23524  conncompid  23662  dislly  23729  locfindis  23762  dfac14lem  23849  txtube  23872  pt1hmeo  24038  ufileu  24151  filufint  24152  uffix  24153  uffixsn  24157  i1fima2sn  25914  ply1rem  26398  noextenddif  27912  noextendlt  27913  noextendgt  27914  cutlt  28205  addsval  28235  negsunif  28328  mulsval  28382  mulsproplem5  28393  mulsproplem6  28394  mulsproplem7  28395  mulsproplem8  28396  mulsuniflem  28422  lnincplng  29149  edglnl  29608  vtxd0nedgb  29956  1loopgrvd2  29971  wlkp1  30147  1wlkdlem2  30616  1conngr  30682  frgrwopregasn  30804  frgrwopregbsn  30805  wlkl0  30855  fconst7v  33101  elrspunsn  33865  selvply1rhmlemb  34037  mplmulmvr  34057  esplyind  34093  rtelextdg2  34245  esumel  34565  actfunsnrndisj  35121  reprsuc  35131  breprexplema  35146  derangsn  35757  erdszelem4  35781  cvmlift2lem9  35898  fv1stcnv  36364  fv2ndcnv  36365  neibastop2lem  36987  ttcsnssg  37143  ttcsnidg  37144  bj-nsnid  37822  bj-snmoore  37871  ismrer1  38596  elpaddatriN  40684  frlmsnic  43430  kelac2  43914  rngunsnply  44018  brtrclfv2  44575  k0004lem3  44997  projf1o  46036  fsneqrn  46049  unirnmapsn  46052  ssmapsn  46054  fconst7  46101  mccllem  46435  limcresiooub  46478  limcresioolb  46479  cnfdmsn  46718  cxpcncf2  46735  dvmptfprodlem  46780  dvnprodlem1  46782  dvnprodlem2  46783  dvnprodlem3  46784  fourierdlem49  46991  prsal  47154  salexct  47170  salgencntex  47179  sge0sn  47215  sge0snmpt  47219  sge0snmptf  47273  caratheodorylem1  47362  hoiprodp1  47424  hoidmv1le  47430  hoidmvlelem1  47431  hoidmvlelem2  47432  hoidmvlelem3  47433  hoidmvlelem4  47434  hspmbllem2  47463  ovnovollem1  47492  ovnovollem2  47493  funressnfv  47939  cfsetsnfsetf  47954  cfsetsnfsetfo  47956  el1fzopredsuc  48222  snlindsntor  49409  lmod1lem1  49425  lmod1lem2  49426  lmod1lem3  49427  lmod1lem4  49428  lmod1lem5  49429  lmod1zr  49431  funcsn  50475