Theorem elsnc 3992

Description: There is exactly 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 3991	. 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 1444   e. wcel 1887   _Vcvv 3045   {csn 3968

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-sn 3969

This theorem is referenced by:  sneqr  4139  opthwiener  4703  opthprc  4882  dmsnn0  5301  dmsnopg  5307  cnvcnvsn  5313  snsn0non  5541  sniota  5573  funconstss  6000  fniniseg  6003  fniniseg2  6005  fsn  6061  fconstfv  6126  eusvobj2  6283  fnse  6913  wfrlem14  7049  fisn  7941  axdc3lem4  8883  axdc4lem  8885  axcclem  8887  ttukeylem7  8945  opelreal  9554  seqid3  12257  seqz  12261  1exp  12301  hashf1lem2  12619  fprodn0f  14045  imasaddfnlem  15434  initoid  15900  termoid  15901  0subg  16842  0nsg  16862  sylow2alem2  17270  gsumval3  17541  gsumzaddlem  17554  kerf1hrm  17971  lsssn0  18171  r0cld  20753  alexsubALTlem2  21063  tgphaus  21131  isusp  21276  i1f1lem  22647  ig1pcl  23127  ig1pclOLD  23133  plyco0  23146  plyeq0lem  23164  plycj  23231  wilthlem2  23994  dchrfi  24183  hsn0elch  26901  h1de2ctlem  27208  atomli  28035  1stpreimas  28286  gsummpt2d  28544  kerunit  28586  qqhval2lem  28785  qqhf  28790  qqhre  28824  esum2dlem  28913  inelpisys  28976  sitgaddlemb  29181  eulerpartlemb  29201  bnj149  29686  subfacp1lem6  29908  ellimits  30677  bj-0nel1  31546  poimirlem18  31958  poimirlem21  31961  poimirlem22  31962  poimirlem31  31971  poimirlem32  31972  itg2addnclem2  31994  ftc1anclem3  32019  0idl  32258  keridl  32265  smprngopr  32285  isdmn3  32307  ellkr  32655  diblss  34738  dihmeetlem4preN  34874  dihmeetlem13N  34887  pw2f1ocnv  35892  fvnonrel  36203  snhesn  36382  snstriedgval  39138  incistruhgr  39171  uspgrloopnb0  39556  umgr2v2enb1  39563  usgra2pthlem1  39720  lindslinindsimp1  40303