Theorem snid 3725

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

Syntax hints:   ∈ wcel 2205  Vcvv 2815  {csn 3694

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-sn 3700

This theorem is referenced by:  vsnid  3726  exsnrex  3736  rabsnt  3771  sneqr  3869  undifexmid  4311  exmidexmid  4314  ss1o0el1  4315  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  unipw  4338  intid  4345  ordtriexmidlem2  4647  ordtriexmid  4648  ontriexmidim  4649  ordtri2orexmid  4650  regexmidlem1  4660  0elsucexmid  4692  ordpwsucexmid  4697  opthprc  4806  fsn  5854  fsn2  5856  fvsn  5884  fvsnun1  5886  acexmidlema  6049  acexmidlemb  6050  acexmidlemab  6052  brtpos0  6496  mapsn  6938  mapsncnv  6943  0elixp  6977  en1  7052  djulclr  7353  djurclr  7354  djulcl  7355  djurcl  7356  djuf1olem  7357  exmidonfinlem  7509  elreal2  8161  1exp  10954  hashinfuni  11165  wrdexb  11261  0bits  12670  ennnfonelemhom  13250  dvef  15704  wlkl1loop  16465  djucllem  16684  bj-d0clsepcl  16807