Theorem snidg 3737

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

Syntax hints:   → wi 4   = wceq 1402   ∈ wcel 2209  {csn 3708

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3714

This theorem is referenced by:  snidb  3738  elsn2g  3741  snnzg  3828  snmg  3829  exmidsssnc  4338  fvunsng  5903  fsnunfv  5910  1stconst  6451  2ndconst  6452  suppsnopdc  6484  tfr0dm  6587  tfrlemibxssdm  6592  tfrlemi14d  6598  tfr1onlembxssdm  6608  tfr1onlemres  6614  tfrcllembxssdm  6621  tfrcllemres  6627  mapsnd  6964  en1uniel  7085  onunsnss  7218  snon0  7243  supsnti  7339  fseq1p1m1  10484  elfzomin  10607  swrds1  11423  fsumsplitsnun  12169  divalgmod  12677  setsslid  13386  bassetsnn  13392  1strbas  13454  srnginvld  13487  lmodvscad  13505  mgm1  13673  mnd1id  13746  0subm  13774  gsumsncmn  14139  gsump1  14140  cnpdis  15326  upgr1edc  16345  uspgr1edc  16464  vtxd0nedgbfi  16523  1loopgrvd2fi  16529  1hegrvtxdg1fi  16533  wlk1walkdom  16583  bj-sels  16923