Theorem elsn 4641

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2108  Vcvv 3480  {csn 4626

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-sn 4627

This theorem is referenced by:  velsn  4642  opthwiener  5519  brsnop  5527  opthprc  5749  dmsnn0  6227  dmsnopg  6233  cnvcnvsn  6239  snsn0non  6509  funconstss  7076  fniniseg  7080  fniniseg2  7082  fsn  7155  fconstfv  7232  eusvobj2  7423  fnse  8158  xpord2pred  8170  xpord2indlem  8172  wfrlem14OLD  8362  fisn  9467  axdc3lem4  10493  axdc4lem  10495  axcclem  10497  opelreal  11170  seqid3  14087  seqz  14091  1exp  14132  hashf1lem2  14495  fprodn0f  16027  imasaddfnlem  17573  initoid  18046  termoid  18047  0subm  18830  smndex1mgm  18920  smndex1n0mnd  18925  grpinvfval  18996  0subg  19169  0subgOLD  19170  0nsg  19187  eqg0subg  19214  kerf1ghm  19265  sylow2alem2  19636  gsumval3  19925  gsumzaddlem  19939  lsssn0  20946  rngqiprngimf1  21310  pzriprnglem8  21499  r0cld  23746  alexsubALTlem2  24056  tgphaus  24125  isusp  24270  i1f1lem  25724  ig1pcl  26218  plyco0  26231  plyeq0lem  26249  plycj  26317  plycjOLD  26319  wilthlem2  27112  dchrfi  27299  mulsval  28135  snstriedgval  29055  incistruhgr  29096  1loopgrnb0  29520  umgr2v2enb1  29544  usgr2pthlem  29783  hsn0elch  31267  h1de2ctlem  31574  atomli  32401  suppiniseg  32695  1stpreimas  32715  gsummpt2d  33052  kerunit  33349  exsslsb  33647  qqhval2lem  33982  qqhf  33987  qqhre  34021  esum2dlem  34093  eulerpartlemb  34370  bnj149  34889  subfacp1lem6  35190  ellimits  35911  weiunse  36469  bj-0nel1  36954  bj-isrvec  37295  poimirlem18  37645  poimirlem21  37648  poimirlem22  37649  poimirlem31  37658  poimirlem32  37659  itg2addnclem2  37679  ftc1anclem3  37702  0idl  38032  keridl  38039  smprngopr  38059  isdmn3  38081  ellkr  39090  diblss  41172  dihmeetlem4preN  41308  dihmeetlem13N  41321  sticksstones11  42157  0prjspnrel  42637  pw2f1ocnv  43049  fvnonrel  43610  snhesn  43799  unirnmapsn  45219  sge0fodjrnlem  46431  isubgr3stgrlem4  47936  usgrexmpl2trifr  47996  lindslinindsimp1  48374