Theorem elsn 4645

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 4644	. 2 ⊢ (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
3	1, 2	ax-mp 5	1 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

Syntax hints:   ↔ wb 205   = wceq 1533   ∈ wcel 2098  Vcvv 3461  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-sn 4631

This theorem is referenced by:  velsn  4646  opthwiener  5516  brsnop  5524  opthprc  5742  dmsnn0  6213  dmsnopg  6219  cnvcnvsn  6225  snsn0non  6496  funconstss  7064  fniniseg  7068  fniniseg2  7070  fsn  7144  fconstfv  7224  eusvobj2  7411  fnse  8138  xpord2pred  8150  xpord2indlem  8152  wfrlem14OLD  8343  fisn  9452  axdc3lem4  10478  axdc4lem  10480  axcclem  10482  opelreal  11155  seqid3  14047  seqz  14051  1exp  14092  hashf1lem2  14453  fprodn0f  15971  imasaddfnlem  17513  initoid  17993  termoid  17994  0subm  18777  smndex1mgm  18867  smndex1n0mnd  18872  grpinvfval  18943  0subg  19114  0subgOLD  19115  0nsg  19132  eqg0subg  19159  kerf1ghm  19210  sylow2alem2  19585  gsumval3  19874  gsumzaddlem  19888  lsssn0  20844  rngqiprngimf1  21207  pzriprnglem8  21431  r0cld  23686  alexsubALTlem2  23996  tgphaus  24065  isusp  24210  i1f1lem  25662  ig1pcl  26158  plyco0  26171  plyeq0lem  26189  plycj  26257  wilthlem2  27046  dchrfi  27233  mulsval  28059  snstriedgval  28923  incistruhgr  28964  1loopgrnb0  29388  umgr2v2enb1  29412  usgr2pthlem  29649  hsn0elch  31130  h1de2ctlem  31437  atomli  32264  suppiniseg  32548  1stpreimas  32567  gsummpt2d  32853  kerunit  33133  qqhval2lem  33713  qqhf  33718  qqhre  33752  esum2dlem  33842  eulerpartlemb  34119  bnj149  34637  subfacp1lem6  34926  ellimits  35637  bj-0nel1  36563  bj-isrvec  36904  poimirlem18  37242  poimirlem21  37245  poimirlem22  37246  poimirlem31  37255  poimirlem32  37256  itg2addnclem2  37276  ftc1anclem3  37299  0idl  37629  keridl  37636  smprngopr  37656  isdmn3  37678  ellkr  38691  diblss  40773  dihmeetlem4preN  40909  dihmeetlem13N  40922  sticksstones11  41759  0prjspnrel  42186  pw2f1ocnv  42600  fvnonrel  43169  snhesn  43358  unirnmapsn  44726  sge0fodjrnlem  45942  lindslinindsimp1  47711