Theorem snid 3700

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 3699	. 2 ⊢ (𝐴 ∈ V ↔ 𝐴 ∈ {𝐴})
3	1, 2	mpbi 145	1 ⊢ 𝐴 ∈ {𝐴}

Syntax hints:   ∈ wcel 2202  Vcvv 2802  {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  vsnid  3701  exsnrex  3711  rabsnt  3746  sneqr  3843  undifexmid  4283  exmidexmid  4286  ss1o0el1  4287  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  unipw  4309  intid  4316  ordtriexmidlem2  4618  ordtriexmid  4619  ontriexmidim  4620  ordtri2orexmid  4621  regexmidlem1  4631  0elsucexmid  4663  ordpwsucexmid  4668  opthprc  4777  fsn  5819  fsn2  5821  fvsn  5849  fvsnun1  5851  acexmidlema  6009  acexmidlemb  6010  acexmidlemab  6012  brtpos0  6418  mapsn  6859  mapsncnv  6864  0elixp  6898  en1  6973  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djuf1olem  7252  exmidonfinlem  7404  elreal2  8050  1exp  10831  hashinfuni  11040  wrdexb  11129  0bits  12525  ennnfonelemhom  13041  dvef  15457  wlkl1loop  16215  djucllem  16422  bj-d0clsepcl  16546