Theorem snidg 4667

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

Syntax hints:   → wi 4   = wceq 1533   ∈ wcel 2098  {csn 4632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-sn 4633

This theorem is referenced by:  snidb  4668  elsn2g  4671  elinsn  4719  snnzg  4783  sneqrg  4845  selsALT  5445  intidg  5463  eldmressnsn  6033  elsnxp  6300  fvressn  7177  fvsnun1  7197  fsnunfv  7202  1stconst  8111  2ndconst  8112  curry1  8115  curry2  8118  suppsnop  8189  mapsnd  8911  en1uniel  9059  en1unielOLD  9060  dif1enlem  9187  dif1enlemOLD  9188  unifpw  9387  sucprcreg  9632  djurf1o  9944  cfsuc  10288  elfzomin  13744  hashrabsn1  14373  swrds1  14656  fsumsplitsnun  15741  lcmfunsnlem1  16615  ramub1lem1  17002  basprssdmsets  17200  acsfiindd  18552  mgm1  18625  mnd1id  18744  odf1o1  19534  gsumconst  19896  lspsolv  21038  mat1ghm  22405  mat1mhm  22406  mavmul0  22474  m1detdiag  22519  mdetrlin  22524  mdetrsca  22525  chpmat1dlem  22757  maxlp  23071  cnpdis  23217  conncompid  23355  dislly  23421  locfindis  23454  dfac14lem  23541  txtube  23564  pt1hmeo  23730  ufileu  23843  filufint  23844  uffix  23845  uffixsn  23849  i1fima2sn  25629  ply1rem  26120  noextenddif  27621  noextendlt  27622  noextendgt  27623  cutlt  27872  addsval  27899  negsunif  27987  mulsval  28029  mulsproplem5  28040  mulsproplem6  28041  mulsproplem7  28042  mulsproplem8  28043  mulsuniflem  28069  edglnl  28976  vtxd0nedgb  29322  1loopgrvd2  29337  wlkp1  29515  1wlkdlem2  29968  1conngr  30024  frgrwopregasn  30146  frgrwopregbsn  30147  wlkl0  30197  elrspunsn  33170  esumel  33699  actfunsnrndisj  34270  reprsuc  34280  breprexplema  34295  derangsn  34813  erdszelem4  34837  cvmlift2lem9  34954  fv1stcnv  35405  fv2ndcnv  35406  neibastop2lem  35877  bj-nsnid  36582  bj-snmoore  36625  ismrer1  37344  elpaddatriN  39308  fnsnbt  41752  frlmsnic  41801  kelac2  42520  rngunsnply  42628  brtrclfv2  43188  k0004lem3  43610  projf1o  44600  fsneq  44609  fsneqrn  44614  unirnmapsn  44617  ssmapsn  44619  fconst7  44670  mccllem  45014  limcresiooub  45059  limcresioolb  45060  cnfdmsn  45299  cxpcncf2  45316  dvmptfprodlem  45361  dvnprodlem1  45363  dvnprodlem2  45364  dvnprodlem3  45365  fourierdlem49  45572  prsal  45735  salexct  45751  salgencntex  45760  sge0sn  45796  sge0snmpt  45800  sge0snmptf  45854  caratheodorylem1  45943  hoiprodp1  46005  hoidmv1le  46011  hoidmvlelem1  46012  hoidmvlelem2  46013  hoidmvlelem3  46014  hoidmvlelem4  46015  hspmbllem2  46044  ovnovollem1  46073  ovnovollem2  46074  funressnfv  46454  cfsetsnfsetf  46469  cfsetsnfsetfo  46471  el1fzopredsuc  46734  snlindsntor  47617  lmod1lem1  47633  lmod1lem2  47634  lmod1lem3  47635  lmod1lem4  47636  lmod1lem5  47637  lmod1zr  47639