Theorem elsn 4573

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-sn 4559

This theorem is referenced by:  velsn  4574  opthwiener  5422  brsnop  5430  opthprc  5642  dmsnn0  6099  dmsnopg  6105  cnvcnvsn  6111  snsn0non  6370  funconstss  6915  fniniseg  6919  fniniseg2  6921  fsn  6989  fconstfv  7070  eusvobj2  7248  fnse  7945  wfrlem14OLD  8124  fisn  9116  axdc3lem4  10140  axdc4lem  10142  axcclem  10144  opelreal  10817  seqid3  13695  seqz  13699  1exp  13740  hashf1lem2  14098  fprodn0f  15629  imasaddfnlem  17156  initoid  17632  termoid  17633  0subm  18371  smndex1mgm  18461  smndex1n0mnd  18466  grpinvfval  18533  0subg  18695  0nsg  18712  sylow2alem2  19138  gsumval3  19423  gsumzaddlem  19437  kerf1ghm  19902  lsssn0  20124  r0cld  22797  alexsubALTlem2  23107  tgphaus  23176  isusp  23321  i1f1lem  24758  ig1pcl  25245  plyco0  25258  plyeq0lem  25276  plycj  25343  wilthlem2  26123  dchrfi  26308  snstriedgval  27311  incistruhgr  27352  1loopgrnb0  27772  umgr2v2enb1  27796  usgr2pthlem  28032  hsn0elch  29511  h1de2ctlem  29818  atomli  30645  suppiniseg  30922  1stpreimas  30940  gsummpt2d  31211  kerunit  31424  qqhval2lem  31831  qqhf  31836  qqhre  31870  esum2dlem  31960  eulerpartlemb  32235  bnj149  32755  subfacp1lem6  33047  xpord2pred  33719  xpord2ind  33721  xpord3pred  33725  ellimits  34139  bj-0nel1  35070  bj-isrvec  35392  poimirlem18  35722  poimirlem21  35725  poimirlem22  35726  poimirlem31  35735  poimirlem32  35736  itg2addnclem2  35756  ftc1anclem3  35779  0idl  36110  keridl  36117  smprngopr  36137  isdmn3  36159  ellkr  37030  diblss  39111  dihmeetlem4preN  39247  dihmeetlem13N  39260  sticksstones11  40040  0prjspnrel  40385  pw2f1ocnv  40775  fvnonrel  41094  snhesn  41283  unirnmapsn  42643  sge0fodjrnlem  43844  lindslinindsimp1  45686