Theorem snidg 4599

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

Syntax hints:   → wi 4   = wceq 1547   ∈ wcel 2119  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-sn 4563

This theorem is referenced by:  snidb  4600  elsn2g  4603  elinsn  4649  snnzg  4713  sneqrg  4777  selsALT  5387  intidg  5403  eldmressnsn  5983  elsnxp  6249  fsneq  6983  fvressn  7112  fnsnbg  7115  fvsnun1  7133  fsnunfv  7138  resf1extb  7881  1stconst  8046  2ndconst  8047  curry1  8050  curry2  8053  suppsnop  8125  mapsnd  8831  en1uniel  8973  dif1enlem  9091  unifpw  9262  sucprcregOLD  9519  djurf1o  9835  cfsuc  10177  elfzomin  13690  hashrabsn1  14334  swrds1  14627  fsumsplitsnun  15715  lcmfunsnlem1  16604  ramub1lem1  16995  basprssdmsets  17189  acsfiindd  18517  mgm1  18624  mnd1id  18746  odf1o1  19545  gsumconst  19907  lspsolv  21143  mat1ghm  22473  mat1mhm  22474  mavmul0  22542  m1detdiag  22587  mdetrlin  22592  mdetrsca  22593  chpmat1dlem  22825  maxlp  23137  cnpdis  23283  conncompid  23421  dislly  23487  locfindis  23520  dfac14lem  23607  txtube  23630  pt1hmeo  23796  ufileu  23909  filufint  23910  uffix  23911  uffixsn  23915  i1fima2sn  25672  ply1rem  26156  noextenddif  27657  noextendlt  27658  noextendgt  27659  cutlt  27949  addsval  27979  negsunif  28072  mulsval  28126  mulsproplem5  28137  mulsproplem6  28138  mulsproplem7  28139  mulsproplem8  28140  mulsuniflem  28166  edglnl  29237  vtxd0nedgb  29582  1loopgrvd2  29597  wlkp1  29773  1wlkdlem2  30233  1conngr  30289  frgrwopregasn  30411  frgrwopregbsn  30412  wlkl0  30462  fconst7v  32719  elrspunsn  33519  selvply1rhmlemb  33710  mplmulmvr  33730  esplyind  33766  rtelextdg2  33918  esumel  34238  actfunsnrndisj  34796  reprsuc  34806  breprexplema  34821  derangsn  35405  erdszelem4  35429  cvmlift2lem9  35546  fv1stcnv  36012  fv2ndcnv  36013  neibastop2lem  36595  ttcsnssg  36751  ttcsnidg  36752  bj-nsnid  37430  bj-snmoore  37478  ismrer1  38212  elpaddatriN  40302  frlmsnic  43033  kelac2  43517  rngunsnply  43621  brtrclfv2  44178  k0004lem3  44600  projf1o  45650  fsneqrn  45663  unirnmapsn  45666  ssmapsn  45668  fconst7  45715  mccllem  46049  limcresiooub  46092  limcresioolb  46093  cnfdmsn  46332  cxpcncf2  46349  dvmptfprodlem  46394  dvnprodlem1  46396  dvnprodlem2  46397  dvnprodlem3  46398  fourierdlem49  46605  prsal  46768  salexct  46784  salgencntex  46793  sge0sn  46829  sge0snmpt  46833  sge0snmptf  46887  caratheodorylem1  46976  hoiprodp1  47038  hoidmv1le  47044  hoidmvlelem1  47045  hoidmvlelem2  47046  hoidmvlelem3  47047  hoidmvlelem4  47048  hspmbllem2  47077  ovnovollem1  47106  ovnovollem2  47107  funressnfv  47513  cfsetsnfsetf  47528  cfsetsnfsetfo  47530  el1fzopredsuc  47796  snlindsntor  48969  lmod1lem1  48985  lmod1lem2  48986  lmod1lem3  48987  lmod1lem4  48988  lmod1lem5  48989  lmod1zr  48991  funcsn  50038