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 206   = wceq 1536   ∈ wcel 2105  Vcvv 3477  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-sn 4631

This theorem is referenced by:  velsn  4646  opthwiener  5523  brsnop  5531  opthprc  5752  dmsnn0  6228  dmsnopg  6234  cnvcnvsn  6240  snsn0non  6510  funconstss  7075  fniniseg  7079  fniniseg2  7081  fsn  7154  fconstfv  7231  eusvobj2  7422  fnse  8156  xpord2pred  8168  xpord2indlem  8170  wfrlem14OLD  8360  fisn  9464  axdc3lem4  10490  axdc4lem  10492  axcclem  10494  opelreal  11167  seqid3  14083  seqz  14087  1exp  14128  hashf1lem2  14491  fprodn0f  16023  imasaddfnlem  17574  initoid  18054  termoid  18055  0subm  18842  smndex1mgm  18932  smndex1n0mnd  18937  grpinvfval  19008  0subg  19181  0subgOLD  19182  0nsg  19199  eqg0subg  19226  kerf1ghm  19277  sylow2alem2  19650  gsumval3  19939  gsumzaddlem  19953  lsssn0  20963  rngqiprngimf1  21327  pzriprnglem8  21516  r0cld  23761  alexsubALTlem2  24071  tgphaus  24140  isusp  24285  i1f1lem  25737  ig1pcl  26232  plyco0  26245  plyeq0lem  26263  plycj  26331  plycjOLD  26333  wilthlem2  27126  dchrfi  27313  mulsval  28149  snstriedgval  29069  incistruhgr  29110  1loopgrnb0  29534  umgr2v2enb1  29558  usgr2pthlem  29795  hsn0elch  31276  h1de2ctlem  31583  atomli  32410  suppiniseg  32700  1stpreimas  32720  gsummpt2d  33034  kerunit  33328  qqhval2lem  33943  qqhf  33948  qqhre  33982  esum2dlem  34072  eulerpartlemb  34349  bnj149  34867  subfacp1lem6  35169  ellimits  35891  weiunse  36450  bj-0nel1  36935  bj-isrvec  37276  poimirlem18  37624  poimirlem21  37627  poimirlem22  37628  poimirlem31  37637  poimirlem32  37638  itg2addnclem2  37658  ftc1anclem3  37681  0idl  38011  keridl  38018  smprngopr  38038  isdmn3  38060  ellkr  39070  diblss  41152  dihmeetlem4preN  41288  dihmeetlem13N  41301  sticksstones11  42137  0prjspnrel  42613  pw2f1ocnv  43025  fvnonrel  43586  snhesn  43775  unirnmapsn  45156  sge0fodjrnlem  46371  isubgr3stgrlem4  47871  usgrexmpl2trifr  47931  lindslinindsimp1  48302