Theorem snid 1830

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49.

Hypothesis

Ref	Expression
snid.1	⊢ A ∈ V

Assertion

Ref	Expression
snid	⊢ A ∈ {A}

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 ⊢ A ∈ V
2		snidb 1829	. 2 ⊢ (A ∈ V ↔ A ∈ {A})
3	1, 2	mpbi 164	1 ⊢ A ∈ {A}

Syntax hints:   ∈ wcel 1092  Vcvv 1348  {csn 1808

This theorem is referenced by:  tpi3 1845  snnz 1846  sneqr 1856  el 1860  rext 1862  opth 1898  opprc3 1908  euuni 1954  reucl 1957  unipw 1960  frirr 2176  sucid 2304  snsn0non 2371  opthprc 2457  fvsn 2879  fsn 2895  fsn2 2896  fnressn 2897  fressnfv 2898  tfrlem11 2959  mapsn 3269  eirrv 3449  inf5 3472  kmlem2 3581  axpowndlem3 3745  fac0 4871  ruclem7 4891  hsn0elch 5155

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-un 1490  df-sn 1811  df-pr 1812

metamath.org