Theorem snidg 4664

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

Syntax hints:   → wi 4   = wceq 1536   ∈ wcel 2105  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sn 4631

This theorem is referenced by:  snidb  4665  elsn2g  4668  elinsn  4714  snnzg  4778  sneqrg  4843  selsALT  5449  intidg  5467  eldmressnsn  6043  elsnxp  6312  fvressn  7181  fvsnun1  7201  fsnunfv  7206  1stconst  8123  2ndconst  8124  curry1  8127  curry2  8130  suppsnop  8201  mapsnd  8924  en1uniel  9067  dif1enlem  9194  dif1enlemOLD  9195  unifpw  9392  sucprcreg  9638  djurf1o  9950  cfsuc  10294  elfzomin  13772  hashrabsn1  14409  swrds1  14700  fsumsplitsnun  15787  lcmfunsnlem1  16670  ramub1lem1  17059  basprssdmsets  17257  acsfiindd  18610  mgm1  18683  mnd1id  18805  odf1o1  19604  gsumconst  19966  lspsolv  21162  mat1ghm  22504  mat1mhm  22505  mavmul0  22573  m1detdiag  22618  mdetrlin  22623  mdetrsca  22624  chpmat1dlem  22856  maxlp  23170  cnpdis  23316  conncompid  23454  dislly  23520  locfindis  23553  dfac14lem  23640  txtube  23663  pt1hmeo  23829  ufileu  23942  filufint  23943  uffix  23944  uffixsn  23948  i1fima2sn  25728  ply1rem  26219  noextenddif  27727  noextendlt  27728  noextendgt  27729  cutlt  27980  addsval  28009  negsunif  28101  mulsval  28149  mulsproplem5  28160  mulsproplem6  28161  mulsproplem7  28162  mulsproplem8  28163  mulsuniflem  28189  edglnl  29174  vtxd0nedgb  29520  1loopgrvd2  29535  wlkp1  29713  1wlkdlem2  30166  1conngr  30222  frgrwopregasn  30344  frgrwopregbsn  30345  wlkl0  30395  elrspunsn  33436  rtelextdg2  33732  esumel  34027  actfunsnrndisj  34598  reprsuc  34608  breprexplema  34623  derangsn  35154  erdszelem4  35178  cvmlift2lem9  35295  fv1stcnv  35757  fv2ndcnv  35758  neibastop2lem  36342  bj-nsnid  37052  bj-snmoore  37095  ismrer1  37824  elpaddatriN  39785  fnsnbt  42249  frlmsnic  42526  kelac2  43053  rngunsnply  43157  brtrclfv2  43716  k0004lem3  44138  projf1o  45139  fsneq  45148  fsneqrn  45153  unirnmapsn  45156  ssmapsn  45158  fconst7  45209  mccllem  45552  limcresiooub  45597  limcresioolb  45598  cnfdmsn  45837  cxpcncf2  45854  dvmptfprodlem  45899  dvnprodlem1  45901  dvnprodlem2  45902  dvnprodlem3  45903  fourierdlem49  46110  prsal  46273  salexct  46289  salgencntex  46298  sge0sn  46334  sge0snmpt  46338  sge0snmptf  46392  caratheodorylem1  46481  hoiprodp1  46543  hoidmv1le  46549  hoidmvlelem1  46550  hoidmvlelem2  46551  hoidmvlelem3  46552  hoidmvlelem4  46553  hspmbllem2  46582  ovnovollem1  46611  ovnovollem2  46612  funressnfv  46992  cfsetsnfsetf  47007  cfsetsnfsetfo  47009  el1fzopredsuc  47274  snlindsntor  48316  lmod1lem1  48332  lmod1lem2  48333  lmod1lem3  48334  lmod1lem4  48335  lmod1lem5  48336  lmod1zr  48338