Theorem snidg 4559

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

Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-sn 4526

This theorem is referenced by:  snidb  4560  elsn2g  4563  elinsn  4606  snnzg  4670  sneqrg  4730  sels  5299  eldmressnsn  5861  elsnxp  6110  fvressn  6901  fvsnun1  6921  fsnunfv  6926  1stconst  7778  2ndconst  7779  curry1  7782  curry2  7785  suppsnop  7827  mapsnd  8433  en1uniel  8564  unifpw  8811  sucprcreg  9049  djurf1o  9326  cfsuc  9668  elfzomin  13104  hashrabsn1  13731  swrds1  14019  fsumsplitsnun  15102  lcmfunsnlem1  15971  ramub1lem1  16352  basprssdmsets  16541  acsfiindd  17779  mgm1  17860  mnd1id  17945  odf1o1  18689  gsumconst  19047  lspsolv  19908  mat1ghm  21088  mat1mhm  21089  mavmul0  21157  m1detdiag  21202  mdetrlin  21207  mdetrsca  21208  chpmat1dlem  21440  maxlp  21752  cnpdis  21898  conncompid  22036  dislly  22102  locfindis  22135  dfac14lem  22222  txtube  22245  pt1hmeo  22411  ufileu  22524  filufint  22525  uffix  22526  uffixsn  22530  i1fima2sn  24284  ply1rem  24764  edglnl  26936  vtxd0nedgb  27278  1loopgrvd2  27293  wlkp1  27471  1wlkdlem2  27923  1conngr  27979  frgrwopregasn  28101  frgrwopregbsn  28102  wlkl0  28152  esumel  31416  actfunsnrndisj  31986  reprsuc  31996  breprexplema  32011  derangsn  32530  erdszelem4  32554  cvmlift2lem9  32671  fv1stcnv  33133  fv2ndcnv  33134  noextenddif  33288  noextendlt  33289  noextendgt  33290  neibastop2lem  33821  bj-nsnid  34486  bj-snmoore  34528  ismrer1  35276  elpaddatriN  37099  fnsnbt  39414  frlmsnic  39453  kelac2  40009  rngunsnply  40117  brtrclfv2  40428  k0004lem3  40852  projf1o  41825  fsneq  41835  fsneqrn  41840  unirnmapsn  41843  ssmapsn  41845  fconst7  41904  mccllem  42239  limcresiooub  42284  limcresioolb  42285  cnfdmsn  42524  cxpcncf2  42541  dvmptfprodlem  42586  dvnprodlem1  42588  dvnprodlem2  42589  dvnprodlem3  42590  fourierdlem49  42797  prsal  42960  salexct  42974  salgencntex  42983  sge0sn  43018  sge0snmpt  43022  sge0snmptf  43076  caratheodorylem1  43165  hoiprodp1  43227  hoidmv1le  43233  hoidmvlelem1  43234  hoidmvlelem2  43235  hoidmvlelem3  43236  hoidmvlelem4  43237  hspmbllem2  43266  ovnovollem1  43295  ovnovollem2  43296  funressnfv  43635  el1fzopredsuc  43882  snlindsntor  44880  lmod1lem1  44896  lmod1lem2  44897  lmod1lem3  44898  lmod1lem4  44899  lmod1lem5  44900  lmod1zr  44902