Theorem snidg 4612

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

Syntax hints:   → wi 4   = wceq 1541   ∈ wcel 2113  {csn 4575

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-sn 4576

This theorem is referenced by:  snidb  4613  elsn2g  4616  elinsn  4662  snnzg  4726  sneqrg  4790  selsALT  5384  intidg  5400  eldmressnsn  5977  elsnxp  6243  fvressn  7101  fnsnbg  7104  fvsnun1  7122  fsnunfv  7127  resf1extb  7870  1stconst  8036  2ndconst  8037  curry1  8040  curry2  8043  suppsnop  8114  mapsnd  8816  en1uniel  8958  dif1enlem  9076  unifpw  9246  sucprcreg  9497  djurf1o  9813  cfsuc  10155  elfzomin  13639  hashrabsn1  14283  swrds1  14576  fsumsplitsnun  15664  lcmfunsnlem1  16550  ramub1lem1  16940  basprssdmsets  17134  acsfiindd  18461  mgm1  18568  mnd1id  18690  odf1o1  19486  gsumconst  19848  lspsolv  21082  mat1ghm  22399  mat1mhm  22400  mavmul0  22468  m1detdiag  22513  mdetrlin  22518  mdetrsca  22519  chpmat1dlem  22751  maxlp  23063  cnpdis  23209  conncompid  23347  dislly  23413  locfindis  23446  dfac14lem  23533  txtube  23556  pt1hmeo  23722  ufileu  23835  filufint  23836  uffix  23837  uffixsn  23841  i1fima2sn  25609  ply1rem  26099  noextenddif  27608  noextendlt  27609  noextendgt  27610  cutlt  27877  addsval  27906  negsunif  27998  mulsval  28049  mulsproplem5  28060  mulsproplem6  28061  mulsproplem7  28062  mulsproplem8  28063  mulsuniflem  28089  edglnl  29123  vtxd0nedgb  29469  1loopgrvd2  29484  wlkp1  29660  1wlkdlem2  30120  1conngr  30176  frgrwopregasn  30298  frgrwopregbsn  30299  wlkl0  30349  fconst7v  32605  elrspunsn  33401  mplmulmvr  33590  esplyind  33613  rtelextdg2  33761  esumel  34081  actfunsnrndisj  34639  reprsuc  34649  breprexplema  34664  derangsn  35235  erdszelem4  35259  cvmlift2lem9  35376  fv1stcnv  35842  fv2ndcnv  35843  neibastop2lem  36425  bj-nsnid  37135  bj-snmoore  37178  ismrer1  37898  elpaddatriN  39922  frlmsnic  42658  kelac2  43182  rngunsnply  43286  brtrclfv2  43844  k0004lem3  44266  projf1o  45318  fsneq  45327  fsneqrn  45332  unirnmapsn  45335  ssmapsn  45337  fconst7  45385  mccllem  45721  limcresiooub  45764  limcresioolb  45765  cnfdmsn  46004  cxpcncf2  46021  dvmptfprodlem  46066  dvnprodlem1  46068  dvnprodlem2  46069  dvnprodlem3  46070  fourierdlem49  46277  prsal  46440  salexct  46456  salgencntex  46465  sge0sn  46501  sge0snmpt  46505  sge0snmptf  46559  caratheodorylem1  46648  hoiprodp1  46710  hoidmv1le  46716  hoidmvlelem1  46717  hoidmvlelem2  46718  hoidmvlelem3  46719  hoidmvlelem4  46720  hspmbllem2  46749  ovnovollem1  46778  ovnovollem2  46779  funressnfv  47167  cfsetsnfsetf  47182  cfsetsnfsetfo  47184  el1fzopredsuc  47449  snlindsntor  48596  lmod1lem1  48612  lmod1lem2  48613  lmod1lem3  48614  lmod1lem4  48615  lmod1lem5  48616  lmod1zr  48618  funcsn  49666