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  17939  termoid  17940  0subm  18720  smndex1mgm  18810  smndex1n0mnd  18815  grpinvfval  18886  0subg  19059  0subgOLD  19060  0nsg  19077  eqg0subg  19104  kerf1ghm  19155  sylow2alem2  19524  gsumval3  19813  gsumzaddlem  19827  lsssn0  20830  rngqiprngimf1  21186  pzriprnglem8  21374  r0cld  23601  alexsubALTlem2  23911  tgphaus  23980  isusp  24125  i1f1lem  25566  ig1pcl  26060  plyco0  26073  plyeq0lem  26091  plycj  26159  plycjOLD  26161  wilthlem2  26955  dchrfi  27142  mulsval  27988  snstriedgval  28941  incistruhgr  28982  1loopgrnb0  29406  umgr2v2enb1  29430  usgr2pthlem  29666  hsn0elch  31150  h1de2ctlem  31457  atomli  32284  suppiniseg  32582  1stpreimas  32602  gsummpt2d  32962  kerunit  33270  exsslsb  33565  qqhval2lem  33944  qqhf  33949  qqhre  33983  esum2dlem  34055  eulerpartlemb  34332  bnj149  34838  subfacp1lem6  35145  ellimits  35871  weiunse  36429  bj-0nel1  36914  bj-isrvec  37255  poimirlem18  37605  poimirlem21  37608  poimirlem22  37609  poimirlem31  37618  poimirlem32  37619  itg2addnclem2  37639  ftc1anclem3  37662  0idl  37992  keridl  37999  smprngopr  38019  isdmn3  38041  ellkr  39055  diblss  41137  dihmeetlem4preN  41273  dihmeetlem13N  41286  sticksstones11  42117  0prjspnrel  42588  pw2f1ocnv  42999  fvnonrel  43559  snhesn  43748  unirnmapsn  45181  sge0fodjrnlem  46387  isubgr3stgrlem4  47941  usgrexmpl2trifr  48001  lindslinindsimp1  48419