Theorem elsnc 4021

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

Syntax hints:   <-> wb 188   = wceq 1438   e. wcel 1869   _Vcvv 3082   {csn 3997

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3084  df-sn 3998

This theorem is referenced by:  sneqr  4165  opthwiener  4720  opthprc  4899  dmsnn0  5318  dmsnopg  5324  cnvcnvsn  5330  snsn0non  5558  sniota  5590  funconstss  6013  fniniseg  6016  fniniseg2  6018  fsn  6074  fconstfv  6139  eusvobj2  6296  fnse  6922  wfrlem14  7055  fisn  7945  axdc3lem4  8885  axdc4lem  8887  axcclem  8889  ttukeylem7  8947  opelreal  9556  seqid3  12258  seqz  12262  1exp  12302  hashf1lem2  12618  fprodn0f  14038  imasaddfnlem  15427  initoid  15893  termoid  15894  0subg  16835  0nsg  16855  sylow2alem2  17263  gsumval3  17534  gsumzaddlem  17547  kerf1hrm  17964  lsssn0  18164  r0cld  20745  alexsubALTlem2  21055  tgphaus  21123  isusp  21268  i1f1lem  22639  ig1pcl  23119  ig1pclOLD  23125  plyco0  23138  plyeq0lem  23156  plycj  23223  wilthlem2  23986  dchrfi  24175  hsn0elch  26893  h1de2ctlem  27200  atomli  28027  1stpreimas  28282  gsummpt2d  28545  kerunit  28588  qqhval2lem  28787  qqhf  28792  qqhre  28826  esum2dlem  28915  inelpisys  28978  sitgaddlemb  29183  eulerpartlemb  29203  bnj149  29688  subfacp1lem6  29910  ellimits  30676  bj-0nel1  31508  poimirlem18  31878  poimirlem21  31881  poimirlem22  31882  poimirlem31  31891  poimirlem32  31892  itg2addnclem2  31914  ftc1anclem3  31939  0idl  32178  keridl  32185  smprngopr  32205  isdmn3  32227  ellkr  32580  diblss  34663  dihmeetlem4preN  34799  dihmeetlem13N  34812  pw2f1ocnv  35818  snhesn  36246  snstriedgval  38807  usgra2pthlem1  38971  lindslinindsimp1  39556