Theorem snidg 4622

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

Syntax hints:   → wi 4   = wceq 1563   ∈ wcel 2145  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-sn 4586

This theorem is referenced by:  snidb  4623  elsn2g  4626  elinsn  4672  snnzg  4736  sneqrg  4800  selsALT  5413  intidg  5429  eldmressnsn  6014  elsnxp  6282  fsneq  7020  fvressn  7149  fnsnbg  7152  fvsnun1  7170  fsnunfv  7175  resf1extb  7919  1stconst  8083  2ndconst  8084  curry1  8087  curry2  8090  suppsnop  8162  mapsnd  8872  en1uniel  9014  dif1enlem  9132  unifpw  9300  sucprcregOLD  9557  djurf1o  9887  cfsuc  10229  elfzomin  13757  hashrabsn1  14401  swrds1  14694  fsumsplitsnun  15796  lcmfunsnlem1  16685  ramub1lem1  17076  basprssdmsets  17271  acsfiindd  18599  mgm1  18706  mnd1id  18828  odf1o1  19633  gsumconst  19995  lspsolv  21236  mat1ghm  22601  mat1mhm  22602  mavmul0  22670  m1detdiag  22715  mdetrlin  22720  mdetrsca  22721  chpmat1dlem  22953  maxlp  23265  cnpdis  23411  conncompid  23549  dislly  23615  locfindis  23648  dfac14lem  23735  txtube  23758  pt1hmeo  23924  ufileu  24037  filufint  24038  uffix  24039  uffixsn  24043  i1fima2sn  25800  ply1rem  26284  noextenddif  27790  noextendlt  27791  noextendgt  27792  cutlt  28083  addsval  28113  negsunif  28206  mulsval  28260  mulsproplem5  28271  mulsproplem6  28272  mulsproplem7  28273  mulsproplem8  28274  mulsuniflem  28300  lnincplng  29014  edglnl  29402  vtxd0nedgb  29747  1loopgrvd2  29762  wlkp1  29938  1wlkdlem2  30398  1conngr  30454  frgrwopregasn  30576  frgrwopregbsn  30577  wlkl0  30627  fconst7v  32877  elrspunsn  33653  selvply1rhmlemb  33826  mplmulmvr  33846  esplyind  33882  rtelextdg2  34034  esumel  34354  actfunsnrndisj  34909  reprsuc  34919  breprexplema  34934  derangsn  35533  erdszelem4  35557  cvmlift2lem9  35674  fv1stcnv  36140  fv2ndcnv  36141  neibastop2lem  36733  ttcsnssg  36889  ttcsnidg  36890  bj-nsnid  37567  bj-snmoore  37615  ismrer1  38349  elpaddatriN  40439  frlmsnic  43170  kelac2  43654  rngunsnply  43758  brtrclfv2  44315  k0004lem3  44737  projf1o  45772  fsneqrn  45785  unirnmapsn  45788  ssmapsn  45790  fconst7  45837  mccllem  46171  limcresiooub  46214  limcresioolb  46215  cnfdmsn  46454  cxpcncf2  46471  dvmptfprodlem  46516  dvnprodlem1  46518  dvnprodlem2  46519  dvnprodlem3  46520  fourierdlem49  46727  prsal  46890  salexct  46906  salgencntex  46915  sge0sn  46951  sge0snmpt  46955  sge0snmptf  47009  caratheodorylem1  47098  hoiprodp1  47160  hoidmv1le  47166  hoidmvlelem1  47167  hoidmvlelem2  47168  hoidmvlelem3  47169  hoidmvlelem4  47170  hspmbllem2  47199  ovnovollem1  47228  ovnovollem2  47229  funressnfv  47635  cfsetsnfsetf  47650  cfsetsnfsetfo  47652  el1fzopredsuc  47918  snlindsntor  49102  lmod1lem1  49118  lmod1lem2  49119  lmod1lem3  49120  lmod1lem4  49121  lmod1lem5  49122  lmod1zr  49124  funcsn  50170