Theorem snidg 4636

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sn 4602

This theorem is referenced by:  snidb  4637  elsn2g  4640  elinsn  4686  snnzg  4750  sneqrg  4815  selsALT  5414  intidg  5432  eldmressnsn  6011  elsnxp  6280  fvressn  7152  fnsnbg  7156  fvsnun1  7174  fsnunfv  7179  resf1extb  7930  1stconst  8099  2ndconst  8100  curry1  8103  curry2  8106  suppsnop  8177  mapsnd  8900  en1uniel  9043  dif1enlem  9170  dif1enlemOLD  9171  unifpw  9367  sucprcreg  9615  djurf1o  9927  cfsuc  10271  elfzomin  13753  hashrabsn1  14392  swrds1  14684  fsumsplitsnun  15771  lcmfunsnlem1  16656  ramub1lem1  17046  basprssdmsets  17240  acsfiindd  18563  mgm1  18636  mnd1id  18758  odf1o1  19553  gsumconst  19915  lspsolv  21104  mat1ghm  22421  mat1mhm  22422  mavmul0  22490  m1detdiag  22535  mdetrlin  22540  mdetrsca  22541  chpmat1dlem  22773  maxlp  23085  cnpdis  23231  conncompid  23369  dislly  23435  locfindis  23468  dfac14lem  23555  txtube  23578  pt1hmeo  23744  ufileu  23857  filufint  23858  uffix  23859  uffixsn  23863  i1fima2sn  25633  ply1rem  26123  noextenddif  27632  noextendlt  27633  noextendgt  27634  cutlt  27892  addsval  27921  negsunif  28013  mulsval  28064  mulsproplem5  28075  mulsproplem6  28076  mulsproplem7  28077  mulsproplem8  28078  mulsuniflem  28104  edglnl  29122  vtxd0nedgb  29468  1loopgrvd2  29483  wlkp1  29661  1wlkdlem2  30119  1conngr  30175  frgrwopregasn  30297  frgrwopregbsn  30298  wlkl0  30348  elrspunsn  33444  rtelextdg2  33761  esumel  34078  actfunsnrndisj  34637  reprsuc  34647  breprexplema  34662  derangsn  35192  erdszelem4  35216  cvmlift2lem9  35333  fv1stcnv  35794  fv2ndcnv  35795  neibastop2lem  36378  bj-nsnid  37088  bj-snmoore  37131  ismrer1  37862  elpaddatriN  39822  frlmsnic  42563  kelac2  43089  rngunsnply  43193  brtrclfv2  43751  k0004lem3  44173  projf1o  45221  fsneq  45230  fsneqrn  45235  unirnmapsn  45238  ssmapsn  45240  fconst7  45288  mccllem  45626  limcresiooub  45671  limcresioolb  45672  cnfdmsn  45911  cxpcncf2  45928  dvmptfprodlem  45973  dvnprodlem1  45975  dvnprodlem2  45976  dvnprodlem3  45977  fourierdlem49  46184  prsal  46347  salexct  46363  salgencntex  46372  sge0sn  46408  sge0snmpt  46412  sge0snmptf  46466  caratheodorylem1  46555  hoiprodp1  46617  hoidmv1le  46623  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  hspmbllem2  46656  ovnovollem1  46685  ovnovollem2  46686  funressnfv  47072  cfsetsnfsetf  47087  cfsetsnfsetfo  47089  el1fzopredsuc  47354  snlindsntor  48447  lmod1lem1  48463  lmod1lem2  48464  lmod1lem3  48465  lmod1lem4  48466  lmod1lem5  48467  lmod1zr  48469