Theorem elsnc 3906

Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)

Hypothesis

Ref	Expression
elsnc.1	|- A e. _V

Assertion

Ref	Expression
elsnc	|- ( A e. { B } <-> A = B )

Proof of Theorem elsnc

Step	Hyp	Ref	Expression
1		elsnc.1	. 2 |- A e. _V
2		elsncg 3905	. 2 |- ( A e. _V -> ( A e. { B } <-> A = B ) )
3	1, 2	ax-mp 5	1 |- ( A e. { B } <-> A = B )

Syntax hints:   <-> wb 184   = wceq 1369   e. wcel 1756   _Vcvv 2977   {csn 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2573  df-v 2979  df-sn 3883

This theorem is referenced by:  sneqr  4045  opthwiener  4598  snsn0non  4842  opthprc  4891  dmsnn0  5309  dmsnopg  5315  cnvcnvsn  5321  sniota  5413  funconstss  5826  fniniseg  5829  fniniseg2  5831  fsn  5886  eusvobj2  6089  fnse  6694  fisn  7682  mapfienOLD  7932  axdc3lem4  8627  axdc4lem  8629  axcclem  8631  ttukeylem7  8689  opelreal  9302  seqid3  11855  seqz  11859  1exp  11898  hashf1lem2  12214  imasaddfnlem  14471  0subg  15711  0nsg  15731  sylow2alem2  16122  gsumval3OLD  16387  gsumval3  16390  gsumzaddlem  16413  gsumzaddlemOLD  16415  kerf1hrm  16836  lsssn0  17034  r0cld  19316  alexsubALTlem2  19625  tgphaus  19692  isusp  19841  i1f1lem  21172  ig1pcl  21652  plyco0  21665  plyeq0lem  21683  plycj  21749  wilthlem2  22412  dchrfi  22599  hsn0elch  24656  h1de2ctlem  24963  atomli  25791  kerunit  26296  qqhval2lem  26415  qqhf  26420  qqhre  26451  eulerpartlemb  26756  subfacp1lem6  27078  wfrlem14  27742  ellimits  27946  itg2addnclem2  28449  ftc1anclem3  28474  0idl  28830  keridl  28837  smprngopr  28857  isdmn3  28879  pw2f1ocnv  29391  usgra2pthlem1  30305  lindslinindsimp1  30996  bnj149  31873  bj-0nel1  32449  ellkr  32739  diblss  34820  dihmeetlem4preN  34956  dihmeetlem13N  34969