Theorem elsn 4595

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4581

This theorem is referenced by:  velsn  4596  opthwiener  5462  brsnop  5470  opthprc  5688  dmsnn0  6165  dmsnopg  6171  cnvcnvsn  6177  snsn0non  6443  funconstss  7001  fniniseg  7005  fniniseg2  7007  fsn  7080  fconstfv  7158  eusvobj2  7350  fnse  8075  xpord2pred  8087  xpord2indlem  8089  fisn  9330  axdc3lem4  10363  axdc4lem  10365  axcclem  10367  opelreal  11041  seqid3  13969  seqz  13973  1exp  14014  hashf1lem2  14379  fprodn0f  15914  imasaddfnlem  17449  initoid  17925  termoid  17926  0subm  18742  smndex1mgm  18832  smndex1n0mnd  18837  grpinvfval  18908  0subg  19081  0nsg  19098  eqg0subg  19125  kerf1ghm  19176  sylow2alem2  19547  gsumval3  19836  gsumzaddlem  19850  lsssn0  20899  rngqiprngimf1  21255  pzriprnglem8  21443  r0cld  23682  alexsubALTlem2  23992  tgphaus  24061  isusp  24205  i1f1lem  25646  ig1pcl  26140  plyco0  26153  plyeq0lem  26171  plycj  26239  plycjOLD  26241  wilthlem2  27035  dchrfi  27222  mulsval  28105  snstriedgval  29111  incistruhgr  29152  1loopgrnb0  29576  umgr2v2enb1  29600  usgr2pthlem  29836  hsn0elch  31323  h1de2ctlem  31630  atomli  32457  suppiniseg  32765  1stpreimas  32785  gsummpt2d  33132  kerunit  33406  exsslsb  33753  qqhval2lem  34138  qqhf  34143  qqhre  34177  esum2dlem  34249  eulerpartlemb  34525  bnj149  35031  subfacp1lem6  35379  ellimits  36102  weiunse  36662  bj-0nel1  37154  bj-isrvec  37499  poimirlem18  37839  poimirlem21  37842  poimirlem22  37843  poimirlem31  37852  poimirlem32  37853  itg2addnclem2  37873  ftc1anclem3  37896  0idl  38226  keridl  38233  smprngopr  38253  isdmn3  38275  ellkr  39359  diblss  41440  dihmeetlem4preN  41576  dihmeetlem13N  41589  sticksstones11  42420  0prjspnrel  42880  pw2f1ocnv  43289  fvnonrel  43848  snhesn  44037  unirnmapsn  45468  sge0fodjrnlem  46670  isubgr3stgrlem4  48225  usgrexmpl2trifr  48293  lindslinindsimp1  48713