Theorem snidg 4614

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4579

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4580

This theorem is referenced by:  snidb  4615  elsn2g  4618  elinsn  4664  snnzg  4728  sneqrg  4793  selsALT  5386  intidg  5404  eldmressnsn  5979  elsnxp  6243  fvressn  7100  fnsnbg  7104  fvsnun1  7122  fsnunfv  7127  resf1extb  7874  1stconst  8040  2ndconst  8041  curry1  8044  curry2  8047  suppsnop  8118  mapsnd  8820  en1uniel  8961  dif1enlem  9080  dif1enlemOLD  9081  unifpw  9264  sucprcreg  9515  djurf1o  9828  cfsuc  10170  elfzomin  13658  hashrabsn1  14299  swrds1  14591  fsumsplitsnun  15680  lcmfunsnlem1  16566  ramub1lem1  16956  basprssdmsets  17150  acsfiindd  18477  mgm1  18550  mnd1id  18672  odf1o1  19469  gsumconst  19831  lspsolv  21068  mat1ghm  22386  mat1mhm  22387  mavmul0  22455  m1detdiag  22500  mdetrlin  22505  mdetrsca  22506  chpmat1dlem  22738  maxlp  23050  cnpdis  23196  conncompid  23334  dislly  23400  locfindis  23433  dfac14lem  23520  txtube  23543  pt1hmeo  23709  ufileu  23822  filufint  23823  uffix  23824  uffixsn  23828  i1fima2sn  25597  ply1rem  26087  noextenddif  27596  noextendlt  27597  noextendgt  27598  cutlt  27863  addsval  27892  negsunif  27984  mulsval  28035  mulsproplem5  28046  mulsproplem6  28047  mulsproplem7  28048  mulsproplem8  28049  mulsuniflem  28075  edglnl  29106  vtxd0nedgb  29452  1loopgrvd2  29467  wlkp1  29643  1wlkdlem2  30100  1conngr  30156  frgrwopregasn  30278  frgrwopregbsn  30279  wlkl0  30329  elrspunsn  33376  rtelextdg2  33693  esumel  34013  actfunsnrndisj  34572  reprsuc  34582  breprexplema  34597  derangsn  35142  erdszelem4  35166  cvmlift2lem9  35283  fv1stcnv  35749  fv2ndcnv  35750  neibastop2lem  36333  bj-nsnid  37043  bj-snmoore  37086  ismrer1  37817  elpaddatriN  39782  frlmsnic  42513  kelac2  43038  rngunsnply  43142  brtrclfv2  43700  k0004lem3  44122  projf1o  45175  fsneq  45184  fsneqrn  45189  unirnmapsn  45192  ssmapsn  45194  fconst7  45242  mccllem  45579  limcresiooub  45624  limcresioolb  45625  cnfdmsn  45864  cxpcncf2  45881  dvmptfprodlem  45926  dvnprodlem1  45928  dvnprodlem2  45929  dvnprodlem3  45930  fourierdlem49  46137  prsal  46300  salexct  46316  salgencntex  46325  sge0sn  46361  sge0snmpt  46365  sge0snmptf  46419  caratheodorylem1  46508  hoiprodp1  46570  hoidmv1le  46576  hoidmvlelem1  46577  hoidmvlelem2  46578  hoidmvlelem3  46579  hoidmvlelem4  46580  hspmbllem2  46609  ovnovollem1  46638  ovnovollem2  46639  funressnfv  47028  cfsetsnfsetf  47043  cfsetsnfsetfo  47045  el1fzopredsuc  47310  snlindsntor  48457  lmod1lem1  48473  lmod1lem2  48474  lmod1lem3  48475  lmod1lem4  48476  lmod1lem5  48477  lmod1zr  48479  funcsn  49527