Theorem elsnc 4040

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 4039	. 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 1398   e. wcel 1823   _Vcvv 3106   {csn 4016

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-sn 4017

This theorem is referenced by:  sneqr  4183  opthwiener  4738  snsn0non  4985  opthprc  5036  dmsnn0  5456  dmsnopg  5462  cnvcnvsn  5468  sniota  5561  funconstss  5981  fniniseg  5984  fniniseg2  5986  fsn  6045  fconstfv  6108  eusvobj2  6263  fnse  6890  fisn  7879  mapfienOLD  8129  axdc3lem4  8824  axdc4lem  8826  axcclem  8828  ttukeylem7  8886  opelreal  9496  seqid3  12133  seqz  12137  1exp  12177  hashf1lem2  12489  imasaddfnlem  15017  initoid  15483  termoid  15484  0subg  16425  0nsg  16445  sylow2alem2  16837  gsumval3OLD  17107  gsumval3  17110  gsumzaddlem  17133  gsumzaddlemOLD  17135  kerf1hrm  17587  lsssn0  17789  r0cld  20405  alexsubALTlem2  20714  tgphaus  20781  isusp  20930  i1f1lem  22262  ig1pcl  22742  plyco0  22755  plyeq0lem  22773  plycj  22840  wilthlem2  23541  dchrfi  23728  hsn0elch  26364  h1de2ctlem  26671  atomli  27499  1stpreimas  27752  gsummpt2d  28006  kerunit  28048  qqhval2lem  28196  qqhf  28201  qqhre  28232  esum2dlem  28321  eulerpartlemb  28571  subfacp1lem6  28893  wfrlem14  29596  ellimits  29788  itg2addnclem2  30307  ftc1anclem3  30332  0idl  30662  keridl  30669  smprngopr  30689  isdmn3  30711  pw2f1ocnv  31218  fprodn0f  31833  usgra2pthlem1  32725  lindslinindsimp1  33312  bnj149  34334  bj-0nel1  34910  ellkr  35211  diblss  37294  dihmeetlem4preN  37430  dihmeetlem13N  37443  snhesn  38259