Theorem elsn 4592

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3436  {csn 4577

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 4578

This theorem is referenced by:  velsn  4593  opthwiener  5457  brsnop  5465  opthprc  5683  dmsnn0  6156  dmsnopg  6162  cnvcnvsn  6168  snsn0non  6433  funconstss  6990  fniniseg  6994  fniniseg2  6996  fsn  7069  fconstfv  7148  eusvobj2  7341  fnse  8066  xpord2pred  8078  xpord2indlem  8080  fisn  9317  axdc3lem4  10347  axdc4lem  10349  axcclem  10351  opelreal  11024  seqid3  13953  seqz  13957  1exp  13998  hashf1lem2  14363  fprodn0f  15898  imasaddfnlem  17432  initoid  17908  termoid  17909  0subm  18691  smndex1mgm  18781  smndex1n0mnd  18786  grpinvfval  18857  0subg  19030  0subgOLD  19031  0nsg  19048  eqg0subg  19075  kerf1ghm  19126  sylow2alem2  19497  gsumval3  19786  gsumzaddlem  19800  lsssn0  20851  rngqiprngimf1  21207  pzriprnglem8  21395  r0cld  23623  alexsubALTlem2  23933  tgphaus  24002  isusp  24147  i1f1lem  25588  ig1pcl  26082  plyco0  26095  plyeq0lem  26113  plycj  26181  plycjOLD  26183  wilthlem2  26977  dchrfi  27164  mulsval  28017  snstriedgval  28983  incistruhgr  29024  1loopgrnb0  29448  umgr2v2enb1  29472  usgr2pthlem  29708  hsn0elch  31192  h1de2ctlem  31499  atomli  32326  suppiniseg  32628  1stpreimas  32648  gsummpt2d  33002  kerunit  33263  exsslsb  33563  qqhval2lem  33948  qqhf  33953  qqhre  33987  esum2dlem  34059  eulerpartlemb  34336  bnj149  34842  subfacp1lem6  35162  ellimits  35888  weiunse  36446  bj-0nel1  36931  bj-isrvec  37272  poimirlem18  37622  poimirlem21  37625  poimirlem22  37626  poimirlem31  37635  poimirlem32  37636  itg2addnclem2  37656  ftc1anclem3  37679  0idl  38009  keridl  38016  smprngopr  38036  isdmn3  38058  ellkr  39072  diblss  41153  dihmeetlem4preN  41289  dihmeetlem13N  41302  sticksstones11  42133  0prjspnrel  42604  pw2f1ocnv  43014  fvnonrel  43574  snhesn  43763  unirnmapsn  45196  sge0fodjrnlem  46401  isubgr3stgrlem4  47957  usgrexmpl2trifr  48025  lindslinindsimp1  48446