Theorem elsn 4616

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  Vcvv 3459  {csn 4601

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-sn 4602

This theorem is referenced by:  velsn  4617  opthwiener  5489  brsnop  5497  opthprc  5718  dmsnn0  6196  dmsnopg  6202  cnvcnvsn  6208  snsn0non  6479  funconstss  7046  fniniseg  7050  fniniseg2  7052  fsn  7125  fconstfv  7204  eusvobj2  7397  fnse  8132  xpord2pred  8144  xpord2indlem  8146  wfrlem14OLD  8336  fisn  9439  axdc3lem4  10467  axdc4lem  10469  axcclem  10471  opelreal  11144  seqid3  14064  seqz  14068  1exp  14109  hashf1lem2  14474  fprodn0f  16007  imasaddfnlem  17542  initoid  18014  termoid  18015  0subm  18795  smndex1mgm  18885  smndex1n0mnd  18890  grpinvfval  18961  0subg  19134  0subgOLD  19135  0nsg  19152  eqg0subg  19179  kerf1ghm  19230  sylow2alem2  19599  gsumval3  19888  gsumzaddlem  19902  lsssn0  20905  rngqiprngimf1  21261  pzriprnglem8  21449  r0cld  23676  alexsubALTlem2  23986  tgphaus  24055  isusp  24200  i1f1lem  25642  ig1pcl  26136  plyco0  26149  plyeq0lem  26167  plycj  26235  plycjOLD  26237  wilthlem2  27031  dchrfi  27218  mulsval  28064  snstriedgval  29017  incistruhgr  29058  1loopgrnb0  29482  umgr2v2enb1  29506  usgr2pthlem  29745  hsn0elch  31229  h1de2ctlem  31536  atomli  32363  suppiniseg  32663  1stpreimas  32683  gsummpt2d  33043  kerunit  33341  exsslsb  33636  qqhval2lem  34012  qqhf  34017  qqhre  34051  esum2dlem  34123  eulerpartlemb  34400  bnj149  34906  subfacp1lem6  35207  ellimits  35928  weiunse  36486  bj-0nel1  36971  bj-isrvec  37312  poimirlem18  37662  poimirlem21  37665  poimirlem22  37666  poimirlem31  37675  poimirlem32  37676  itg2addnclem2  37696  ftc1anclem3  37719  0idl  38049  keridl  38056  smprngopr  38076  isdmn3  38098  ellkr  39107  diblss  41189  dihmeetlem4preN  41325  dihmeetlem13N  41338  sticksstones11  42169  0prjspnrel  42650  pw2f1ocnv  43061  fvnonrel  43621  snhesn  43810  unirnmapsn  45238  sge0fodjrnlem  46445  isubgr3stgrlem4  47981  usgrexmpl2trifr  48041  lindslinindsimp1  48433