Theorem elsnc 3797

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 3796	. 2 |- ( A e. _V -> ( A e. { B } <-> A = B ) )
3	1, 2	ax-mp 8	1 |- ( A e. { B } <-> A = B )

Syntax hints:   <-> wb 177   = wceq 1649   e. wcel 1721   _Vcvv 2916   {csn 3774

This theorem is referenced by:  sneqr  3926  opthwiener  4418  snsn0non  4659  opthprc  4884  dmsnn0  5294  dmsnopg  5300  cnvcnvsn  5306  sniota  5404  funconstss  5807  fniniseg  5810  fniniseg2  5812  fsn  5865  fnse  6422  eusvobj2  6541  fisn  7390  mapfien  7609  axdc3lem4  8289  axdc4lem  8291  axcclem  8293  ttukeylem7  8351  opelreal  8961  seqid3  11322  seqz  11326  1exp  11364  hashf1lem2  11660  imasaddfnlem  13708  0subg  14920  0nsg  14940  sylow2alem2  15207  gsumval3  15469  gsumzaddlem  15481  lsssn0  15979  r0cld  17723  alexsubALTlem2  18032  tgphaus  18099  isusp  18244  i1f1lem  19534  ig1pcl  20051  plyco0  20064  plyeq0lem  20082  plycj  20148  wilthlem2  20805  dchrfi  20992  hsn0elch  22703  h1de2ctlem  23010  atomli  23838  kerunit  24214  kerf1hrm  24215  qqhval2lem  24318  qqhf  24323  qqhre  24339  sibfof  24607  subfacp1lem6  24824  wfrlem14  25483  ellimits  25664  itg2addnclem2  26156  0idl  26525  keridl  26532  smprngopr  26552  isdmn3  26574  pw2f1ocnv  26998  usgra2pthlem1  28040  bnj149  28952  ellkr  29572  diblss  31653  dihmeetlem4preN  31789  dihmeetlem13N  31802

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-sn 3780