Theorem snid 3698

Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.)

Hypothesis

Ref	Expression
snid.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
snid	⊢ 𝐴 ∈ {𝐴}

Proof of Theorem snid

Step	Hyp	Ref	Expression
1		snid.1	. 2 ⊢ 𝐴 ∈ V
2		snidb 3697	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 145	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2200  Vcvv 2800  {csn 3667

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2802  df-sn 3673

This theorem is referenced by:  vsnid  3699  exsnrex  3709  rabsnt  3744  sneqr  3841  undifexmid  4281  exmidexmid  4284  ss1o0el1  4285  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  unipw  4307  intid  4314  ordtriexmidlem2  4616  ordtriexmid  4617  ontriexmidim  4618  ordtri2orexmid  4619  regexmidlem1  4629  0elsucexmid  4661  ordpwsucexmid  4666  opthprc  4775  fsn  5815  fsn2  5817  fvsn  5844  fvsnun1  5846  acexmidlema  6004  acexmidlemb  6005  acexmidlemab  6007  brtpos0  6413  mapsn  6854  mapsncnv  6859  0elixp  6893  en1  6968  djulclr  7242  djurclr  7243  djulcl  7244  djurcl  7245  djuf1olem  7246  exmidonfinlem  7397  elreal2  8043  1exp  10823  hashinfuni  11032  wrdexb  11118  0bits  12513  ennnfonelemhom  13029  dvef  15444  wlkl1loop  16169  djucllem  16346  bj-d0clsepcl  16470