Theorem snid 3614

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

Syntax hints:   ∈ wcel 2141  Vcvv 2730  {csn 3583

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 3589

This theorem is referenced by:  vsnid  3615  exsnrex  3625  rabsnt  3658  sneqr  3747  undifexmid  4179  exmidexmid  4182  ss1o0el1  4183  exmidundif  4192  exmidundifim  4193  unipw  4202  intid  4209  ordtriexmidlem2  4504  ordtriexmid  4505  ontriexmidim  4506  ordtri2orexmid  4507  regexmidlem1  4517  0elsucexmid  4549  ordpwsucexmid  4554  opthprc  4662  fsn  5668  fsn2  5670  fvsn  5691  fvsnun1  5693  acexmidlema  5844  acexmidlemb  5845  acexmidlemab  5847  brtpos0  6231  mapsn  6668  mapsncnv  6673  0elixp  6707  en1  6777  djulclr  7026  djurclr  7027  djulcl  7028  djurcl  7029  djuf1olem  7030  exmidonfinlem  7170  elreal2  7792  1exp  10505  hashinfuni  10711  ennnfonelemhom  12370  dvef  13482  djucllem  13835  bj-d0clsepcl  13960  exmid1stab  14033