Theorem snidg 4613

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2111  {csn 4576

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sn 4577

This theorem is referenced by:  snidb  4614  elsn2g  4617  elinsn  4663  snnzg  4727  sneqrg  4791  selsALT  5382  intidg  5398  eldmressnsn  5973  elsnxp  6238  fvressn  7095  fnsnbg  7098  fvsnun1  7116  fsnunfv  7121  resf1extb  7864  1stconst  8030  2ndconst  8031  curry1  8034  curry2  8037  suppsnop  8108  mapsnd  8810  en1uniel  8951  dif1enlem  9069  unifpw  9239  sucprcreg  9490  djurf1o  9803  cfsuc  10145  elfzomin  13634  hashrabsn1  14278  swrds1  14571  fsumsplitsnun  15659  lcmfunsnlem1  16545  ramub1lem1  16935  basprssdmsets  17129  acsfiindd  18456  mgm1  18563  mnd1id  18685  odf1o1  19482  gsumconst  19844  lspsolv  21078  mat1ghm  22396  mat1mhm  22397  mavmul0  22465  m1detdiag  22510  mdetrlin  22515  mdetrsca  22516  chpmat1dlem  22748  maxlp  23060  cnpdis  23206  conncompid  23344  dislly  23410  locfindis  23443  dfac14lem  23530  txtube  23553  pt1hmeo  23719  ufileu  23832  filufint  23833  uffix  23834  uffixsn  23838  i1fima2sn  25606  ply1rem  26096  noextenddif  27605  noextendlt  27606  noextendgt  27607  cutlt  27874  addsval  27903  negsunif  27995  mulsval  28046  mulsproplem5  28057  mulsproplem6  28058  mulsproplem7  28059  mulsproplem8  28060  mulsuniflem  28086  edglnl  29119  vtxd0nedgb  29465  1loopgrvd2  29480  wlkp1  29656  1wlkdlem2  30113  1conngr  30169  frgrwopregasn  30291  frgrwopregbsn  30292  wlkl0  30342  fconst7v  32598  elrspunsn  33389  rtelextdg2  33735  esumel  34055  actfunsnrndisj  34613  reprsuc  34623  breprexplema  34638  derangsn  35202  erdszelem4  35226  cvmlift2lem9  35343  fv1stcnv  35809  fv2ndcnv  35810  neibastop2lem  36393  bj-nsnid  37103  bj-snmoore  37146  ismrer1  37877  elpaddatriN  39841  frlmsnic  42572  kelac2  43097  rngunsnply  43201  brtrclfv2  43759  k0004lem3  44181  projf1o  45233  fsneq  45242  fsneqrn  45247  unirnmapsn  45250  ssmapsn  45252  fconst7  45300  mccllem  45636  limcresiooub  45679  limcresioolb  45680  cnfdmsn  45919  cxpcncf2  45936  dvmptfprodlem  45981  dvnprodlem1  45983  dvnprodlem2  45984  dvnprodlem3  45985  fourierdlem49  46192  prsal  46355  salexct  46371  salgencntex  46380  sge0sn  46416  sge0snmpt  46420  sge0snmptf  46474  caratheodorylem1  46563  hoiprodp1  46625  hoidmv1le  46631  hoidmvlelem1  46632  hoidmvlelem2  46633  hoidmvlelem3  46634  hoidmvlelem4  46635  hspmbllem2  46664  ovnovollem1  46693  ovnovollem2  46694  funressnfv  47073  cfsetsnfsetf  47088  cfsetsnfsetfo  47090  el1fzopredsuc  47355  snlindsntor  48502  lmod1lem1  48518  lmod1lem2  48519  lmod1lem3  48520  lmod1lem4  48521  lmod1lem5  48522  lmod1zr  48524  funcsn  49572