Theorem snidg 4592

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

Syntax hints:   → wi 4   = wceq 1539   ∈ wcel 2108  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4559

This theorem is referenced by:  snidb  4593  elsn2g  4596  elinsn  4643  snnzg  4707  sneqrg  4767  sels  5351  eldmressnsn  5923  elsnxp  6183  fvressn  7016  fvsnun1  7036  fsnunfv  7041  1stconst  7911  2ndconst  7912  curry1  7915  curry2  7918  suppsnop  7965  mapsnd  8632  en1uniel  8772  en1unielOLD  8773  dif1enlem  8905  unifpw  9052  sucprcreg  9290  djurf1o  9602  cfsuc  9944  elfzomin  13387  hashrabsn1  14017  swrds1  14307  fsumsplitsnun  15395  lcmfunsnlem1  16270  ramub1lem1  16655  basprssdmsets  16853  acsfiindd  18186  mgm1  18257  mnd1id  18342  odf1o1  19092  gsumconst  19450  lspsolv  20320  mat1ghm  21540  mat1mhm  21541  mavmul0  21609  m1detdiag  21654  mdetrlin  21659  mdetrsca  21660  chpmat1dlem  21892  maxlp  22206  cnpdis  22352  conncompid  22490  dislly  22556  locfindis  22589  dfac14lem  22676  txtube  22699  pt1hmeo  22865  ufileu  22978  filufint  22979  uffix  22980  uffixsn  22984  i1fima2sn  24749  ply1rem  25233  edglnl  27416  vtxd0nedgb  27758  1loopgrvd2  27773  wlkp1  27951  1wlkdlem2  28403  1conngr  28459  frgrwopregasn  28581  frgrwopregbsn  28582  wlkl0  28632  esumel  31915  actfunsnrndisj  32485  reprsuc  32495  breprexplema  32510  derangsn  33032  erdszelem4  33056  cvmlift2lem9  33173  fv1stcnv  33657  fv2ndcnv  33658  noextenddif  33798  noextendlt  33799  noextendgt  33800  addsval  34053  neibastop2lem  34476  bj-nsnid  35168  bj-snmoore  35211  ismrer1  35923  elpaddatriN  37744  fnsnbt  40134  frlmsnic  40188  kelac2  40806  rngunsnply  40914  brtrclfv2  41224  k0004lem3  41648  projf1o  42625  fsneq  42635  fsneqrn  42640  unirnmapsn  42643  ssmapsn  42645  fconst7  42701  mccllem  43028  limcresiooub  43073  limcresioolb  43074  cnfdmsn  43313  cxpcncf2  43330  dvmptfprodlem  43375  dvnprodlem1  43377  dvnprodlem2  43378  dvnprodlem3  43379  fourierdlem49  43586  prsal  43749  salexct  43763  salgencntex  43772  sge0sn  43807  sge0snmpt  43811  sge0snmptf  43865  caratheodorylem1  43954  hoiprodp1  44016  hoidmv1le  44022  hoidmvlelem1  44023  hoidmvlelem2  44024  hoidmvlelem3  44025  hoidmvlelem4  44026  hspmbllem2  44055  ovnovollem1  44084  ovnovollem2  44085  funressnfv  44424  cfsetsnfsetf  44439  cfsetsnfsetfo  44441  el1fzopredsuc  44705  snlindsntor  45700  lmod1lem1  45716  lmod1lem2  45717  lmod1lem3  45718  lmod1lem4  45719  lmod1lem5  45720  lmod1zr  45722