Theorem snid 3739

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

Syntax hints:   ∈ wcel 2209  Vcvv 2821  {csn 3708

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 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-sn 3714

This theorem is referenced by:  vsnid  3740  exsnrex  3750  rabsnt  3785  sneqr  3883  undifexmid  4328  exmidexmid  4331  ss1o0el1  4332  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  unipw  4355  intid  4362  ordtriexmidlem2  4665  ordtriexmid  4666  ontriexmidim  4667  ordtri2orexmid  4668  regexmidlem1  4678  0elsucexmid  4710  ordpwsucexmid  4715  opthprc  4824  fsn  5874  fsn2  5876  fvsn  5904  fvsnun1  5906  acexmidlema  6070  acexmidlemb  6071  acexmidlemab  6073  brtpos0  6517  mapsn  6966  mapsncnv  6971  0elixp  7005  en1  7080  djulclr  7383  djurclr  7384  djulcl  7385  djurcl  7386  djuf1olem  7387  exmidonfinlem  7539  elreal2  8191  1exp  10988  hashinfuni  11199  wrdexb  11299  0bits  12709  ennnfonelemhom  13289  dvef  15811  wlkl1loop  16582  djucllem  16811  bj-d0clsepcl  16934