Theorem elsn 4599

Description: There is exactly one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)

Hypothesis

Ref	Expression
elsn.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
elsn	⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Proof of Theorem elsn

Step	Hyp	Ref	Expression
1		elsn.1	. 2 ⊢ 𝐴 ∈ V
2		elsng 4598	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  Vcvv 3451  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-sn 4585

This theorem is used by:  velsn  4600  opthwiener  5487  brsnop  5496  opthprc  5715  dmsnn0  6208  dmsnopg  6214  cnvcnvsn  6220  snsn0non  6489  funconstss  7055  fniniseg  7059  fniniseg2  7061  fsn  7136  fconstfv  7218  eusvobj2  7412  fnse  8150  xpord2pred  8162  xpord2indlem  8164  fisn  9419  axdc3lem4  10531  axdc4lem  10533  axcclem  10535  opelreal  11215  seqid3  14189  seqz  14193  1exp  14234  hashf1lem2  14601  fprodn0f  16158  imasaddfnlem  17700  initoid  18176  termoid  18177  0subm  19013  smndex1mgm  19106  smndex1n0mnd  19111  grpinvfval  19189  0subg  19362  0nsg  19379  eqg0subg  19411  kerf1ghm  19461  sylow2alem2  19832  gsumval3  20121  gsumzaddlem  20135  lsssn0  21223  rngqiprngimf1  21596  pzriprnglem8  21794  r0cld  24057  alexsubALTlem2  24367  tgphaus  24436  isusp  24580  i1f1lem  26010  ig1pcl  26497  plyco0  26510  plyeq0lem  26529  plycj  26596  wilthlem2  27396  dchrfi  27582  mulsval  28495  snstriedgval  29616  incistruhgr  29657  1loopgrnb0  30083  umgr2v2enb1  30107  usgr2pthlem  30349  hsn0elch  31850  h1de2ctlem  32157  atomli  32984  suppiniseg  33279  1stpreimas  33299  gsummpt2d  33610  kerunit  33886  exsslsb  34229  qqhval2lem  34613  qqhf  34618  qqhre  34652  esum2dlem  34724  eulerpartlemb  35000  bnj149  35505  subfacp1lem6  35950  ellimits  36672  nmulprop  36939  weiunse  37256  bj-0nel1  37866  bj-isrvec  38215  poimirlem18  38556  poimirlem21  38559  poimirlem22  38560  poimirlem31  38569  poimirlem32  38570  itg2addnclem2  38590  ftc1anclem3  38613  0idl  38959  keridl  38966  smprngopr  38986  isdmn3  39008  ellkr  40146  diblss  42227  dihmeetlem4preN  42363  dihmeetlem13N  42376  sticksstones11  43206  0prjspnrel  43663  pw2f1ocnv  44043  fvnonrel  44596  snhesn  44785  unirnmapsn  46226  sge0fodjrnlem  47425  tmachlem-agreeprod  47946  isubgr3stgrlem4  49066  usgrexmpl2trifr  49134  smprngprmrng  49435  isidom3  49441  lindslinindsimp1  49568