Theorem snidg 4624

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

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109  {csn 4589

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4590

This theorem is referenced by:  snidb  4625  elsn2g  4628  elinsn  4674  snnzg  4738  sneqrg  4803  selsALT  5399  intidg  5417  eldmressnsn  5995  elsnxp  6264  fvressn  7134  fnsnbg  7138  fvsnun1  7156  fsnunfv  7161  resf1extb  7910  1stconst  8079  2ndconst  8080  curry1  8083  curry2  8086  suppsnop  8157  mapsnd  8859  en1uniel  9000  dif1enlem  9120  dif1enlemOLD  9121  unifpw  9306  sucprcreg  9554  djurf1o  9866  cfsuc  10210  elfzomin  13698  hashrabsn1  14339  swrds1  14631  fsumsplitsnun  15721  lcmfunsnlem1  16607  ramub1lem1  16997  basprssdmsets  17191  acsfiindd  18512  mgm1  18585  mnd1id  18707  odf1o1  19502  gsumconst  19864  lspsolv  21053  mat1ghm  22370  mat1mhm  22371  mavmul0  22439  m1detdiag  22484  mdetrlin  22489  mdetrsca  22490  chpmat1dlem  22722  maxlp  23034  cnpdis  23180  conncompid  23318  dislly  23384  locfindis  23417  dfac14lem  23504  txtube  23527  pt1hmeo  23693  ufileu  23806  filufint  23807  uffix  23808  uffixsn  23812  i1fima2sn  25581  ply1rem  26071  noextenddif  27580  noextendlt  27581  noextendgt  27582  cutlt  27840  addsval  27869  negsunif  27961  mulsval  28012  mulsproplem5  28023  mulsproplem6  28024  mulsproplem7  28025  mulsproplem8  28026  mulsuniflem  28052  edglnl  29070  vtxd0nedgb  29416  1loopgrvd2  29431  wlkp1  29609  1wlkdlem2  30067  1conngr  30123  frgrwopregasn  30245  frgrwopregbsn  30246  wlkl0  30296  elrspunsn  33400  rtelextdg2  33717  esumel  34037  actfunsnrndisj  34596  reprsuc  34606  breprexplema  34621  derangsn  35157  erdszelem4  35181  cvmlift2lem9  35298  fv1stcnv  35764  fv2ndcnv  35765  neibastop2lem  36348  bj-nsnid  37058  bj-snmoore  37101  ismrer1  37832  elpaddatriN  39797  frlmsnic  42528  kelac2  43054  rngunsnply  43158  brtrclfv2  43716  k0004lem3  44138  projf1o  45191  fsneq  45200  fsneqrn  45205  unirnmapsn  45208  ssmapsn  45210  fconst7  45258  mccllem  45595  limcresiooub  45640  limcresioolb  45641  cnfdmsn  45880  cxpcncf2  45897  dvmptfprodlem  45942  dvnprodlem1  45944  dvnprodlem2  45945  dvnprodlem3  45946  fourierdlem49  46153  prsal  46316  salexct  46332  salgencntex  46341  sge0sn  46377  sge0snmpt  46381  sge0snmptf  46435  caratheodorylem1  46524  hoiprodp1  46586  hoidmv1le  46592  hoidmvlelem1  46593  hoidmvlelem2  46594  hoidmvlelem3  46595  hoidmvlelem4  46596  hspmbllem2  46625  ovnovollem1  46654  ovnovollem2  46655  funressnfv  47044  cfsetsnfsetf  47059  cfsetsnfsetfo  47061  el1fzopredsuc  47326  snlindsntor  48460  lmod1lem1  48476  lmod1lem2  48477  lmod1lem3  48478  lmod1lem4  48479  lmod1lem5  48480  lmod1zr  48482  funcsn  49530