Theorem snidg 4472

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

Syntax hints:   → wi 4   = wceq 1507   ∈ wcel 2050  {csn 4442

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-sn 4443

This theorem is referenced by:  snidb  4473  elsn2g  4476  elinsn  4521  snnzg  4585  sneqrg  4645  sels  5191  eldmressnsn  5742  elsnxp  5982  fvressn  6749  fvsnun1  6771  fsnunfv  6778  1stconst  7605  2ndconst  7606  curry1  7609  curry2  7612  suppsnop  7649  mapsnd  8250  en1uniel  8380  unifpw  8624  sucprcreg  8862  djurf1o  9138  cfsuc  9479  elfzomin  12927  hashrabsn1  13551  swrds1  13847  fsumsplitsnun  14973  lcmfunsnlem1  15840  ramub1lem1  16221  basprssdmsets  16408  acsfiindd  17648  mgm1  17728  mnd1id  17803  odf1o1  18461  gsumconst  18810  lspsolv  19640  mat1ghm  20799  mat1mhm  20800  mavmul0  20868  m1detdiag  20913  mdetrlin  20918  mdetrsca  20919  chpmat1dlem  21150  maxlp  21462  cnpdis  21608  conncompid  21746  dislly  21812  locfindis  21845  dfac14lem  21932  txtube  21955  pt1hmeo  22121  ufileu  22234  filufint  22235  uffix  22236  uffixsn  22240  i1fima2sn  23987  ply1rem  24463  edglnl  26634  vtxd0nedgb  26976  1loopgrvd2  26991  wlkp1  27172  1wlkdlem2  27670  1conngr  27726  frgrwopregasn  27853  frgrwopregbsn  27854  wlkl0  27923  esumel  30950  actfunsnrndisj  31524  reprsuc  31534  breprexplema  31549  derangsn  32002  erdszelem4  32026  cvmlift2lem9  32143  fv1stcnv  32540  fv2ndcnv  32541  noextenddif  32696  noextendlt  32697  noextendgt  32698  neibastop2lem  33229  bj-nsnid  33871  bj-snmoore  33916  ismrer1  34558  elpaddatriN  36384  fnsnbt  38565  frlmsnic  38586  kelac2  39061  rngunsnply  39169  brtrclfv2  39435  k0004lem3  39862  projf1o  40885  fsneq  40895  fsneqrn  40900  unirnmapsn  40903  ssmapsn  40905  fconst7  40969  mccllem  41310  limcresiooub  41355  limcresioolb  41356  cnfdmsn  41596  cxpcncf2  41614  dvmptfprodlem  41660  dvnprodlem1  41662  dvnprodlem2  41663  dvnprodlem3  41664  fourierdlem49  41872  prsal  42035  salexct  42049  salgencntex  42058  sge0sn  42093  sge0snmpt  42097  sge0snmptf  42151  caratheodorylem1  42240  hoiprodp1  42302  hoidmv1le  42308  hoidmvlelem1  42309  hoidmvlelem2  42310  hoidmvlelem3  42311  hoidmvlelem4  42312  hspmbllem2  42341  ovnovollem1  42370  ovnovollem2  42371  funressnfv  42684  el1fzopredsuc  42932  snlindsntor  43894  lmod1lem1  43910  lmod1lem2  43911  lmod1lem3  43912  lmod1lem4  43913  lmod1lem5  43914  lmod1zr  43916