Theorem elsn 4597

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

Syntax hints:   ↔ wb 208   = wceq 1560   ∈ wcel 2142  Vcvv 3454  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-sn 4583

This theorem is referenced by:  velsn  4598  opthwiener  5483  brsnop  5492  opthprc  5711  dmsnn0  6194  dmsnopg  6200  cnvcnvsn  6206  snsn0non  6472  funconstss  7037  fniniseg  7041  fniniseg2  7043  fsn  7117  fconstfv  7196  eusvobj2  7388  fnse  8113  xpord2pred  8125  xpord2indlem  8127  fisn  9373  axdc3lem4  10410  axdc4lem  10412  axcclem  10414  opelreal  11088  seqid3  14059  seqz  14063  1exp  14104  hashf1lem2  14469  fprodn0f  16021  imasaddfnlem  17558  initoid  18034  termoid  18035  0subm  18851  smndex1mgm  18944  smndex1n0mnd  18949  grpinvfval  19020  0subg  19193  0nsg  19210  eqg0subg  19237  kerf1ghm  19287  sylow2alem2  19658  gsumval3  19947  gsumzaddlem  19961  lsssn0  21015  rngqiprngimf1  21370  pzriprnglem8  21540  r0cld  23798  alexsubALTlem2  24108  tgphaus  24177  isusp  24321  i1f1lem  25751  ig1pcl  26239  plyco0  26252  plyeq0lem  26270  plycj  26337  plycjOLD  26339  wilthlem2  27133  dchrfi  27319  mulsval  28202  snstriedgval  29239  incistruhgr  29280  1loopgrnb0  29703  umgr2v2enb1  29727  usgr2pthlem  29963  hsn0elch  31451  h1de2ctlem  31758  atomli  32585  suppiniseg  32888  1stpreimas  32908  gsummpt2d  33229  kerunit  33511  exsslsb  33894  qqhval2lem  34278  qqhf  34283  qqhre  34317  esum2dlem  34389  eulerpartlemb  34665  bnj149  35170  subfacp1lem6  35535  ellimits  36258  nmulprop  36540  weiunse  36828  bj-0nel1  37438  bj-isrvec  37786  poimirlem18  38137  poimirlem21  38140  poimirlem22  38141  poimirlem31  38150  poimirlem32  38151  itg2addnclem2  38171  ftc1anclem3  38194  0idl  38524  keridl  38531  smprngopr  38551  isdmn3  38573  ellkr  39713  diblss  41794  dihmeetlem4preN  41930  dihmeetlem13N  41943  sticksstones11  42773  0prjspnrel  43209  pw2f1ocnv  43614  fvnonrel  44173  snhesn  44362  unirnmapsn  45790  sge0fodjrnlem  46990  isubgr3stgrlem4  48591  usgrexmpl2trifr  48659  lindslinindsimp1  49079