Theorem elsn 4600

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3444  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4586

This theorem is referenced by:  velsn  4601  opthwiener  5469  brsnop  5477  opthprc  5695  dmsnn0  6168  dmsnopg  6174  cnvcnvsn  6180  snsn0non  6447  funconstss  7010  fniniseg  7014  fniniseg2  7016  fsn  7089  fconstfv  7168  eusvobj2  7361  fnse  8089  xpord2pred  8101  xpord2indlem  8103  fisn  9354  axdc3lem4  10382  axdc4lem  10384  axcclem  10386  opelreal  11059  seqid3  13987  seqz  13991  1exp  14032  hashf1lem2  14397  fprodn0f  15933  imasaddfnlem  17467  initoid  17943  termoid  17944  0subm  18726  smndex1mgm  18816  smndex1n0mnd  18821  grpinvfval  18892  0subg  19065  0subgOLD  19066  0nsg  19083  eqg0subg  19110  kerf1ghm  19161  sylow2alem2  19532  gsumval3  19821  gsumzaddlem  19835  lsssn0  20886  rngqiprngimf1  21242  pzriprnglem8  21430  r0cld  23658  alexsubALTlem2  23968  tgphaus  24037  isusp  24182  i1f1lem  25623  ig1pcl  26117  plyco0  26130  plyeq0lem  26148  plycj  26216  plycjOLD  26218  wilthlem2  27012  dchrfi  27199  mulsval  28052  snstriedgval  29018  incistruhgr  29059  1loopgrnb0  29483  umgr2v2enb1  29507  usgr2pthlem  29743  hsn0elch  31227  h1de2ctlem  31534  atomli  32361  suppiniseg  32659  1stpreimas  32679  gsummpt2d  33032  kerunit  33290  exsslsb  33585  qqhval2lem  33964  qqhf  33969  qqhre  34003  esum2dlem  34075  eulerpartlemb  34352  bnj149  34858  subfacp1lem6  35165  ellimits  35891  weiunse  36449  bj-0nel1  36934  bj-isrvec  37275  poimirlem18  37625  poimirlem21  37628  poimirlem22  37629  poimirlem31  37638  poimirlem32  37639  itg2addnclem2  37659  ftc1anclem3  37682  0idl  38012  keridl  38019  smprngopr  38039  isdmn3  38061  ellkr  39075  diblss  41157  dihmeetlem4preN  41293  dihmeetlem13N  41306  sticksstones11  42137  0prjspnrel  42608  pw2f1ocnv  43019  fvnonrel  43579  snhesn  43768  unirnmapsn  45201  sge0fodjrnlem  46407  isubgr3stgrlem4  47961  usgrexmpl2trifr  48021  lindslinindsimp1  48439