Theorem elsnc 3889

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 3888	. 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 1362   e. wcel 1755   _Vcvv 2962   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-sn 3866

This theorem is referenced by:  sneqr  4028  opthwiener  4581  snsn0non  4824  opthprc  4873  dmsnn0  5292  dmsnopg  5298  cnvcnvsn  5304  sniota  5396  funconstss  5809  fniniseg  5812  fniniseg2  5814  fsn  5868  eusvobj2  6072  fnse  6678  fisn  7665  mapfienOLD  7915  axdc3lem4  8610  axdc4lem  8612  axcclem  8614  ttukeylem7  8672  opelreal  9284  seqid3  11833  seqz  11837  1exp  11876  hashf1lem2  12192  imasaddfnlem  14448  0subg  15685  0nsg  15705  sylow2alem2  16096  gsumval3OLD  16361  gsumval3  16364  gsumzaddlem  16387  gsumzaddlemOLD  16389  lsssn0  16950  r0cld  19152  alexsubALTlem2  19461  tgphaus  19528  isusp  19677  i1f1lem  21008  ig1pcl  21531  plyco0  21544  plyeq0lem  21562  plycj  21628  wilthlem2  22291  dchrfi  22478  hsn0elch  24473  h1de2ctlem  24780  atomli  25608  kerunit  26143  kerf1hrm  26144  qqhval2lem  26263  qqhf  26268  qqhre  26299  eulerpartlemb  26598  subfacp1lem6  26920  wfrlem14  27583  ellimits  27787  itg2addnclem2  28285  ftc1anclem3  28310  0idl  28666  keridl  28673  smprngopr  28693  isdmn3  28715  pw2f1ocnv  29228  usgra2pthlem1  30143  lindslinindsimp1  30697  bnj149  31567  bj-0nel1  32024  ellkr  32304  diblss  34385  dihmeetlem4preN  34521  dihmeetlem13N  34534