Theorem snidg 4682

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

Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2108  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  snidb  4683  elsn2g  4686  elinsn  4735  snnzg  4799  sneqrg  4864  selsALT  5459  intidg  5477  eldmressnsn  6053  elsnxp  6322  fvressn  7196  fvsnun1  7216  fsnunfv  7221  1stconst  8141  2ndconst  8142  curry1  8145  curry2  8148  suppsnop  8219  mapsnd  8944  en1uniel  9093  en1unielOLD  9094  dif1enlem  9222  dif1enlemOLD  9223  unifpw  9425  sucprcreg  9670  djurf1o  9982  cfsuc  10326  elfzomin  13788  hashrabsn1  14423  swrds1  14714  fsumsplitsnun  15803  lcmfunsnlem1  16684  ramub1lem1  17073  basprssdmsets  17271  acsfiindd  18623  mgm1  18696  mnd1id  18815  odf1o1  19614  gsumconst  19976  lspsolv  21168  mat1ghm  22510  mat1mhm  22511  mavmul0  22579  m1detdiag  22624  mdetrlin  22629  mdetrsca  22630  chpmat1dlem  22862  maxlp  23176  cnpdis  23322  conncompid  23460  dislly  23526  locfindis  23559  dfac14lem  23646  txtube  23669  pt1hmeo  23835  ufileu  23948  filufint  23949  uffix  23950  uffixsn  23954  i1fima2sn  25734  ply1rem  26225  noextenddif  27731  noextendlt  27732  noextendgt  27733  cutlt  27984  addsval  28013  negsunif  28105  mulsval  28153  mulsproplem5  28164  mulsproplem6  28165  mulsproplem7  28166  mulsproplem8  28167  mulsuniflem  28193  edglnl  29178  vtxd0nedgb  29524  1loopgrvd2  29539  wlkp1  29717  1wlkdlem2  30170  1conngr  30226  frgrwopregasn  30348  frgrwopregbsn  30349  wlkl0  30399  elrspunsn  33422  rtelextdg2  33718  esumel  34011  actfunsnrndisj  34582  reprsuc  34592  breprexplema  34607  derangsn  35138  erdszelem4  35162  cvmlift2lem9  35279  fv1stcnv  35740  fv2ndcnv  35741  neibastop2lem  36326  bj-nsnid  37036  bj-snmoore  37079  ismrer1  37798  elpaddatriN  39760  fnsnbt  42225  frlmsnic  42495  kelac2  43022  rngunsnply  43130  brtrclfv2  43689  k0004lem3  44111  projf1o  45104  fsneq  45113  fsneqrn  45118  unirnmapsn  45121  ssmapsn  45123  fconst7  45174  mccllem  45518  limcresiooub  45563  limcresioolb  45564  cnfdmsn  45803  cxpcncf2  45820  dvmptfprodlem  45865  dvnprodlem1  45867  dvnprodlem2  45868  dvnprodlem3  45869  fourierdlem49  46076  prsal  46239  salexct  46255  salgencntex  46264  sge0sn  46300  sge0snmpt  46304  sge0snmptf  46358  caratheodorylem1  46447  hoiprodp1  46509  hoidmv1le  46515  hoidmvlelem1  46516  hoidmvlelem2  46517  hoidmvlelem3  46518  hoidmvlelem4  46519  hspmbllem2  46548  ovnovollem1  46577  ovnovollem2  46578  funressnfv  46958  cfsetsnfsetf  46973  cfsetsnfsetfo  46975  el1fzopredsuc  47240  snlindsntor  48200  lmod1lem1  48216  lmod1lem2  48217  lmod1lem3  48218  lmod1lem4  48219  lmod1lem5  48220  lmod1zr  48222