Theorem snid 3612

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

Syntax hints:   ∈ wcel 2141  Vcvv 2730  {csn 3581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-v 2732  df-sn 3587

This theorem is referenced by:  vsnid  3613  exsnrex  3623  rabsnt  3656  sneqr  3745  undifexmid  4177  exmidexmid  4180  ss1o0el1  4181  exmidundif  4190  exmidundifim  4191  unipw  4200  intid  4207  ordtriexmidlem2  4502  ordtriexmid  4503  ontriexmidim  4504  ordtri2orexmid  4505  regexmidlem1  4515  0elsucexmid  4547  ordpwsucexmid  4552  opthprc  4660  fsn  5665  fsn2  5667  fvsn  5688  fvsnun1  5690  acexmidlema  5841  acexmidlemb  5842  acexmidlemab  5844  brtpos0  6228  mapsn  6664  mapsncnv  6669  0elixp  6703  en1  6773  djulclr  7022  djurclr  7023  djulcl  7024  djurcl  7025  djuf1olem  7026  exmidonfinlem  7157  elreal2  7779  1exp  10492  hashinfuni  10698  ennnfonelemhom  12357  dvef  13403  djucllem  13756  bj-d0clsepcl  13882  exmid1stab  13955