Theorem elsn 4582

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2110  Vcvv 3431  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-sn 4568

This theorem is referenced by:  velsn  4583  opthwiener  5432  brsnop  5440  opthprc  5652  dmsnn0  6109  dmsnopg  6115  cnvcnvsn  6121  snsn0non  6384  funconstss  6930  fniniseg  6934  fniniseg2  6936  fsn  7004  fconstfv  7085  eusvobj2  7264  fnse  7965  wfrlem14OLD  8144  fisn  9164  axdc3lem4  10210  axdc4lem  10212  axcclem  10214  opelreal  10887  seqid3  13765  seqz  13769  1exp  13810  hashf1lem2  14168  fprodn0f  15699  imasaddfnlem  17237  initoid  17714  termoid  17715  0subm  18454  smndex1mgm  18544  smndex1n0mnd  18549  grpinvfval  18616  0subg  18778  0nsg  18795  sylow2alem2  19221  gsumval3  19506  gsumzaddlem  19520  kerf1ghm  19985  lsssn0  20207  r0cld  22887  alexsubALTlem2  23197  tgphaus  23266  isusp  23411  i1f1lem  24851  ig1pcl  25338  plyco0  25351  plyeq0lem  25369  plycj  25436  wilthlem2  26216  dchrfi  26401  snstriedgval  27406  incistruhgr  27447  1loopgrnb0  27867  umgr2v2enb1  27891  usgr2pthlem  28127  hsn0elch  29606  h1de2ctlem  29913  atomli  30740  suppiniseg  31016  1stpreimas  31034  gsummpt2d  31305  kerunit  31518  qqhval2lem  31927  qqhf  31932  qqhre  31966  esum2dlem  32056  eulerpartlemb  32331  bnj149  32851  subfacp1lem6  33143  xpord2pred  33788  xpord2ind  33790  xpord3pred  33794  ellimits  34208  bj-0nel1  35139  bj-isrvec  35461  poimirlem18  35791  poimirlem21  35794  poimirlem22  35795  poimirlem31  35804  poimirlem32  35805  itg2addnclem2  35825  ftc1anclem3  35848  0idl  36179  keridl  36186  smprngopr  36206  isdmn3  36228  ellkr  37099  diblss  39180  dihmeetlem4preN  39316  dihmeetlem13N  39329  sticksstones11  40109  0prjspnrel  40461  pw2f1ocnv  40856  fvnonrel  41175  snhesn  41364  unirnmapsn  42724  sge0fodjrnlem  43925  lindslinindsimp1  45767