Theorem elsnc 4051

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 4050	. 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 1379   e. wcel 1767   _Vcvv 3113   {csn 4027

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-sn 4028

This theorem is referenced by:  sneqr  4194  opthwiener  4749  snsn0non  4996  opthprc  5046  dmsnn0  5471  dmsnopg  5477  cnvcnvsn  5483  sniota  5576  funconstss  5997  fniniseg  6000  fniniseg2  6002  fsn  6057  eusvobj2  6275  fnse  6897  fisn  7883  mapfienOLD  8134  axdc3lem4  8829  axdc4lem  8831  axcclem  8833  ttukeylem7  8891  opelreal  9503  seqid3  12115  seqz  12119  1exp  12159  hashf1lem2  12467  imasaddfnlem  14779  0subg  16021  0nsg  16041  sylow2alem2  16434  gsumval3OLD  16699  gsumval3  16702  gsumzaddlem  16725  gsumzaddlemOLD  16727  kerf1hrm  17175  lsssn0  17377  r0cld  19974  alexsubALTlem2  20283  tgphaus  20350  isusp  20499  i1f1lem  21831  ig1pcl  22311  plyco0  22324  plyeq0lem  22342  plycj  22408  wilthlem2  23071  dchrfi  23258  hsn0elch  25842  h1de2ctlem  26149  atomli  26977  kerunit  27476  qqhval2lem  27598  qqhf  27603  qqhre  27634  eulerpartlemb  27947  subfacp1lem6  28269  wfrlem14  28933  ellimits  29137  itg2addnclem2  29644  ftc1anclem3  29669  0idl  30025  keridl  30032  smprngopr  30052  isdmn3  30074  pw2f1ocnv  30583  usgra2pthlem1  31822  lindslinindsimp1  32131  bnj149  33012  bj-0nel1  33590  ellkr  33886  diblss  35967  dihmeetlem4preN  36103  dihmeetlem13N  36116