Theorem snidg 4605

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

Syntax hints:   → wi 4   = wceq 1542   ∈ wcel 2114  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4569

This theorem is referenced by:  snidb  4606  elsn2g  4609  elinsn  4655  snnzg  4719  sneqrg  4783  selsALT  5386  intidg  5402  eldmressnsn  5981  elsnxp  6247  fvressn  7107  fnsnbg  7110  fvsnun1  7128  fsnunfv  7133  resf1extb  7876  1stconst  8041  2ndconst  8042  curry1  8045  curry2  8048  suppsnop  8119  mapsnd  8825  en1uniel  8967  dif1enlem  9085  unifpw  9256  sucprcreg  9510  djurf1o  9826  cfsuc  10168  elfzomin  13681  hashrabsn1  14325  swrds1  14618  fsumsplitsnun  15706  lcmfunsnlem1  16595  ramub1lem1  16986  basprssdmsets  17180  acsfiindd  18508  mgm1  18615  mnd1id  18737  odf1o1  19536  gsumconst  19898  lspsolv  21131  mat1ghm  22457  mat1mhm  22458  mavmul0  22526  m1detdiag  22571  mdetrlin  22576  mdetrsca  22577  chpmat1dlem  22809  maxlp  23121  cnpdis  23267  conncompid  23405  dislly  23471  locfindis  23504  dfac14lem  23591  txtube  23614  pt1hmeo  23780  ufileu  23893  filufint  23894  uffix  23895  uffixsn  23899  i1fima2sn  25656  ply1rem  26143  noextenddif  27651  noextendlt  27652  noextendgt  27653  cutlt  27943  addsval  27973  negsunif  28066  mulsval  28120  mulsproplem5  28131  mulsproplem6  28132  mulsproplem7  28133  mulsproplem8  28134  mulsuniflem  28160  edglnl  29231  vtxd0nedgb  29577  1loopgrvd2  29592  wlkp1  29768  1wlkdlem2  30228  1conngr  30284  frgrwopregasn  30406  frgrwopregbsn  30407  wlkl0  30457  fconst7v  32713  elrspunsn  33509  mplmulmvr  33703  esplyind  33739  rtelextdg2  33892  esumel  34212  actfunsnrndisj  34770  reprsuc  34780  breprexplema  34795  derangsn  35373  erdszelem4  35397  cvmlift2lem9  35514  fv1stcnv  35980  fv2ndcnv  35981  neibastop2lem  36563  ttcsnssg  36719  ttcsnidg  36720  bj-nsnid  37390  bj-snmoore  37438  ismrer1  38170  elpaddatriN  40260  frlmsnic  42996  kelac2  43508  rngunsnply  43612  brtrclfv2  44169  k0004lem3  44591  projf1o  45641  fsneq  45650  fsneqrn  45655  unirnmapsn  45658  ssmapsn  45660  fconst7  45708  mccllem  46042  limcresiooub  46085  limcresioolb  46086  cnfdmsn  46325  cxpcncf2  46342  dvmptfprodlem  46387  dvnprodlem1  46389  dvnprodlem2  46390  dvnprodlem3  46391  fourierdlem49  46598  prsal  46761  salexct  46777  salgencntex  46786  sge0sn  46822  sge0snmpt  46826  sge0snmptf  46880  caratheodorylem1  46969  hoiprodp1  47031  hoidmv1le  47037  hoidmvlelem1  47038  hoidmvlelem2  47039  hoidmvlelem3  47040  hoidmvlelem4  47041  hspmbllem2  47070  ovnovollem1  47099  ovnovollem2  47100  funressnfv  47488  cfsetsnfsetf  47503  cfsetsnfsetfo  47505  el1fzopredsuc  47771  snlindsntor  48944  lmod1lem1  48960  lmod1lem2  48961  lmod1lem3  48962  lmod1lem4  48963  lmod1lem5  48964  lmod1zr  48966  funcsn  50013