Theorem snidg 3618

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

Syntax hints:   → wi 4   = wceq 1353   ∈ wcel 2146  {csn 3589

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-sn 3595

This theorem is referenced by:  snidb  3619  elsn2g  3622  snnzg  3706  snmg  3707  exmidsssnc  4198  fvunsng  5702  fsnunfv  5709  1stconst  6212  2ndconst  6213  tfr0dm  6313  tfrlemibxssdm  6318  tfrlemi14d  6324  tfr1onlembxssdm  6334  tfr1onlemres  6340  tfrcllembxssdm  6347  tfrcllemres  6353  en1uniel  6794  onunsnss  6906  snon0  6925  supsnti  6994  fseq1p1m1  10062  elfzomin  10174  fsumsplitsnun  11393  divalgmod  11897  setsslid  12477  1strbas  12528  srnginvld  12555  lmodvscad  12569  mgm1  12653  mnd1id  12709  0subm  12731  cnpdis  13311  bj-sels  14224