Theorem snidg 4621

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4585

This theorem is used by:  snidb  4622  elsn2g  4625  elinsn  4671  snnzg  4735  sneqrg  4799  selsALT  5409  intidg  5425  eldmressnsn  6015  elsnxp  6287  fsneq  7026  fvressn  7158  fnsnbg  7161  fvsnun1  7179  fsnunfv  7184  resf1extb  7935  1stconst  8100  2ndconst  8101  curry1  8104  curry2  8107  suppsnop  8179  mapsnd  8898  en1uniel  9041  dif1enlem  9159  unifpw  9328  sucprcregOLD  9585  djurf1o  9975  cfsuc  10316  elfzomin  13852  hashrabsn1  14498  swrds1  14796  fsumsplitsnun  15901  lcmfunsnlem1  16792  ramub1lem1  17184  basprssdmsets  17379  acsfiindd  18707  mgm1  18816  mnd1id  18954  odf1o1  19766  gsumconst  20128  lspsolv  21401  mat1ghm  22778  mat1mhm  22779  mavmul0  22847  m1detdiag  22892  mdetrlin  22897  mdetrsca  22898  chpmat1dlem  23133  maxlp  23445  cnpdis  23591  conncompid  23729  dislly  23796  locfindis  23829  dfac14lem  23916  txtube  23939  pt1hmeo  24105  ufileu  24218  filufint  24219  uffix  24220  uffixsn  24224  i1fima2sn  25981  ply1rem  26464  noextenddif  28007  noextendlt  28008  noextendgt  28009  cutlt  28300  addsval  28330  negsunif  28423  mulsval  28477  mulsproplem5  28488  mulsproplem6  28489  mulsproplem7  28490  mulsproplem8  28491  mulsuniflem  28517  lnincplng  29244  edglnl  29703  vtxd0nedgb  30051  1loopgrvd2  30066  wlkp1  30242  1wlkdlem2  30711  1conngr  30777  frgrwopregasn  30899  frgrwopregbsn  30900  wlkl0  30950  fconst7v  33196  elrspunsn  33961  selvply1rhmlemb  34133  mplmulmvr  34153  esplyind  34189  rtelextdg2  34341  esumel  34661  actfunsnrndisj  35217  reprsuc  35227  breprexplema  35242  derangsn  35904  erdszelem4  35928  cvmlift2lem9  36045  fv1stcnv  36511  fv2ndcnv  36512  neibastop2lem  37118  ttcsnssg  37274  ttcsnidg  37275  bj-nsnid  37953  bj-snmoore  38002  ismrer1  38740  elpaddatriN  40828  frlmsnic  43566  kelac2  44025  rngunsnply  44129  brtrclfv2  44686  k0004lem3  45108  projf1o  46154  fsneqrn  46167  unirnmapsn  46170  ssmapsn  46172  fconst7  46219  mccllem  46553  limcresiooub  46596  limcresioolb  46597  cnfdmsn  46836  cxpcncf2  46853  dvmptfprodlem  46898  dvnprodlem1  46900  dvnprodlem2  46901  dvnprodlem3  46902  fourierdlem49  47109  prsal  47272  salexct  47288  salgencntex  47297  sge0sn  47333  sge0snmpt  47337  sge0snmptf  47391  caratheodorylem1  47480  hoiprodp1  47542  hoidmv1le  47548  hoidmvlelem1  47549  hoidmvlelem2  47550  hoidmvlelem3  47551  hoidmvlelem4  47552  hspmbllem2  47581  ovnovollem1  47610  ovnovollem2  47611  funressnfv  48057  cfsetsnfsetf  48072  cfsetsnfsetfo  48074  el1fzopredsuc  48340  snlindsntor  49527  lmod1lem1  49543  lmod1lem2  49544  lmod1lem3  49545  lmod1lem4  49546  lmod1lem5  49547  lmod1zr  49549  funcsn  50593