Theorem elsn 4576

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

Syntax hints:   ↔ wb 205   = wceq 1539   ∈ wcel 2106  Vcvv 3432  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-sn 4562

This theorem is referenced by:  velsn  4577  opthwiener  5428  brsnop  5436  opthprc  5651  dmsnn0  6110  dmsnopg  6116  cnvcnvsn  6122  snsn0non  6385  funconstss  6933  fniniseg  6937  fniniseg2  6939  fsn  7007  fconstfv  7088  eusvobj2  7268  fnse  7974  wfrlem14OLD  8153  fisn  9186  axdc3lem4  10209  axdc4lem  10211  axcclem  10213  opelreal  10886  seqid3  13767  seqz  13771  1exp  13812  hashf1lem2  14170  fprodn0f  15701  imasaddfnlem  17239  initoid  17716  termoid  17717  0subm  18456  smndex1mgm  18546  smndex1n0mnd  18551  grpinvfval  18618  0subg  18780  0nsg  18797  sylow2alem2  19223  gsumval3  19508  gsumzaddlem  19522  kerf1ghm  19987  lsssn0  20209  r0cld  22889  alexsubALTlem2  23199  tgphaus  23268  isusp  23413  i1f1lem  24853  ig1pcl  25340  plyco0  25353  plyeq0lem  25371  plycj  25438  wilthlem2  26218  dchrfi  26403  snstriedgval  27408  incistruhgr  27449  1loopgrnb0  27869  umgr2v2enb1  27893  usgr2pthlem  28131  hsn0elch  29610  h1de2ctlem  29917  atomli  30744  suppiniseg  31020  1stpreimas  31038  gsummpt2d  31309  kerunit  31522  qqhval2lem  31931  qqhf  31936  qqhre  31970  esum2dlem  32060  eulerpartlemb  32335  bnj149  32855  subfacp1lem6  33147  xpord2pred  33792  xpord2ind  33794  xpord3pred  33798  ellimits  34212  bj-0nel1  35143  bj-isrvec  35465  poimirlem18  35795  poimirlem21  35798  poimirlem22  35799  poimirlem31  35808  poimirlem32  35809  itg2addnclem2  35829  ftc1anclem3  35852  0idl  36183  keridl  36190  smprngopr  36210  isdmn3  36232  ellkr  37103  diblss  39184  dihmeetlem4preN  39320  dihmeetlem13N  39333  sticksstones11  40112  0prjspnrel  40464  pw2f1ocnv  40859  fvnonrel  41205  snhesn  41394  unirnmapsn  42754  sge0fodjrnlem  43954  lindslinindsimp1  45798