Theorem snidg 4627

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

Syntax hints:   → wi 4   = wceq 1570   ∈ wcel 2143  {csn 4590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4591

This theorem is referenced by:  snidb  4628  elsn2g  4631  elinsn  4677  snnzg  4741  sneqrg  4805  selsALT  5424  intidg  5440  eldmressnsn  6025  elsnxp  6294  fsneq  7032  fvressn  7161  fnsnbg  7164  fvsnun1  7182  fsnunfv  7187  resf1extb  7932  1stconst  8096  2ndconst  8097  curry1  8100  curry2  8103  suppsnop  8175  mapsnd  8885  en1uniel  9027  dif1enlem  9145  unifpw  9313  sucprcregOLD  9570  djurf1o  9900  cfsuc  10242  elfzomin  13768  hashrabsn1  14412  swrds1  14706  fsumsplitsnun  15808  lcmfunsnlem1  16696  ramub1lem1  17087  basprssdmsets  17282  acsfiindd  18610  mgm1  18717  mnd1id  18839  odf1o1  19643  gsumconst  20005  lspsolv  21248  mat1ghm  22621  mat1mhm  22622  mavmul0  22690  m1detdiag  22735  mdetrlin  22740  mdetrsca  22741  chpmat1dlem  22973  maxlp  23285  cnpdis  23431  conncompid  23569  dislly  23635  locfindis  23668  dfac14lem  23755  txtube  23778  pt1hmeo  23944  ufileu  24057  filufint  24058  uffix  24059  uffixsn  24063  i1fima2sn  25820  ply1rem  26304  noextenddif  27810  noextendlt  27811  noextendgt  27812  cutlt  28103  addsval  28133  negsunif  28226  mulsval  28280  mulsproplem5  28291  mulsproplem6  28292  mulsproplem7  28293  mulsproplem8  28294  mulsuniflem  28320  lnincplng  29044  edglnl  29471  vtxd0nedgb  29816  1loopgrvd2  29831  wlkp1  30007  1wlkdlem2  30467  1conngr  30523  frgrwopregasn  30645  frgrwopregbsn  30646  wlkl0  30696  fconst7v  32943  elrspunsn  33715  selvply1rhmlemb  33887  mplmulmvr  33907  esplyind  33943  rtelextdg2  34095  esumel  34415  actfunsnrndisj  34970  reprsuc  34980  breprexplema  34995  derangsn  35640  erdszelem4  35664  cvmlift2lem9  35781  fv1stcnv  36247  fv2ndcnv  36248  neibastop2lem  36849  ttcsnssg  37005  ttcsnidg  37006  bj-nsnid  37684  bj-snmoore  37733  ismrer1  38467  elpaddatriN  40555  frlmsnic  43288  kelac2  43772  rngunsnply  43876  brtrclfv2  44433  k0004lem3  44855  projf1o  45894  fsneqrn  45907  unirnmapsn  45910  ssmapsn  45912  fconst7  45959  mccllem  46293  limcresiooub  46336  limcresioolb  46337  cnfdmsn  46576  cxpcncf2  46593  dvmptfprodlem  46638  dvnprodlem1  46640  dvnprodlem2  46641  dvnprodlem3  46642  fourierdlem49  46849  prsal  47012  salexct  47028  salgencntex  47037  sge0sn  47073  sge0snmpt  47077  sge0snmptf  47131  caratheodorylem1  47220  hoiprodp1  47282  hoidmv1le  47288  hoidmvlelem1  47289  hoidmvlelem2  47290  hoidmvlelem3  47291  hoidmvlelem4  47292  hspmbllem2  47321  ovnovollem1  47350  ovnovollem2  47351  funressnfv  47757  cfsetsnfsetf  47772  cfsetsnfsetfo  47774  el1fzopredsuc  48040  snlindsntor  49228  lmod1lem1  49244  lmod1lem2  49245  lmod1lem3  49246  lmod1lem4  49247  lmod1lem5  49248  lmod1zr  49250  funcsn  50296