Theorem snid 3638

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

Syntax hints:   ∈ wcel 2160  Vcvv 2752  {csn 3607

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 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-v 2754  df-sn 3613

This theorem is referenced by:  vsnid  3639  exsnrex  3649  rabsnt  3682  sneqr  3775  undifexmid  4211  exmidexmid  4214  ss1o0el1  4215  exmidundif  4224  exmidundifim  4225  exmid1stab  4226  unipw  4235  intid  4242  ordtriexmidlem2  4537  ordtriexmid  4538  ontriexmidim  4539  ordtri2orexmid  4540  regexmidlem1  4550  0elsucexmid  4582  ordpwsucexmid  4587  opthprc  4695  fsn  5708  fsn2  5710  fvsn  5731  fvsnun1  5733  acexmidlema  5886  acexmidlemb  5887  acexmidlemab  5889  brtpos0  6276  mapsn  6715  mapsncnv  6720  0elixp  6754  en1  6824  djulclr  7077  djurclr  7078  djulcl  7079  djurcl  7080  djuf1olem  7081  exmidonfinlem  7221  elreal2  7858  1exp  10579  hashinfuni  10788  ennnfonelemhom  12465  dvef  14640  djucllem  15005  bj-d0clsepcl  15130