Theorem elsn 4606

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2146  Vcvv 3457  {csn 4591

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-sn 4592

This theorem is used by:  velsn  4607  opthwiener  5499  brsnop  5508  opthprc  5727  dmsnn0  6210  dmsnopg  6216  cnvcnvsn  6222  snsn0non  6491  funconstss  7055  fniniseg  7059  fniniseg2  7061  fsn  7135  fconstfv  7217  eusvobj2  7411  fnse  8135  xpord2pred  8147  xpord2indlem  8149  fisn  9394  axdc3lem4  10452  axdc4lem  10454  axcclem  10456  opelreal  11132  seqid3  14102  seqz  14106  1exp  14147  hashf1lem2  14513  fprodn0f  16070  imasaddfnlem  17606  initoid  18082  termoid  18083  0subm  18915  smndex1mgm  19008  smndex1n0mnd  19013  grpinvfval  19091  0subg  19264  0nsg  19281  eqg0subg  19313  kerf1ghm  19363  sylow2alem2  19734  gsumval3  20023  gsumzaddlem  20037  lsssn0  21121  rngqiprngimf1  21492  pzriprnglem8  21690  r0cld  23948  alexsubALTlem2  24258  tgphaus  24327  isusp  24471  i1f1lem  25901  ig1pcl  26389  plyco0  26402  plyeq0lem  26420  plycj  26487  plycjOLD  26489  wilthlem2  27286  dchrfi  27472  mulsval  28355  snstriedgval  29445  incistruhgr  29486  1loopgrnb0  29912  umgr2v2enb1  29936  usgr2pthlem  30178  hsn0elch  31673  h1de2ctlem  31980  atomli  32807  suppiniseg  33104  1stpreimas  33124  gsummpt2d  33435  kerunit  33711  exsslsb  34053  qqhval2lem  34437  qqhf  34442  qqhre  34476  esum2dlem  34548  eulerpartlemb  34825  bnj149  35330  subfacp1lem6  35716  ellimits  36439  nmulprop  36721  weiunse  37038  bj-0nel1  37648  bj-isrvec  37997  poimirlem18  38348  poimirlem21  38351  poimirlem22  38352  poimirlem31  38361  poimirlem32  38362  itg2addnclem2  38382  ftc1anclem3  38405  0idl  38736  keridl  38743  smprngopr  38763  isdmn3  38785  ellkr  39923  diblss  42004  dihmeetlem4preN  42140  dihmeetlem13N  42153  sticksstones11  42983  0prjspnrel  43419  pw2f1ocnv  43824  fvnonrel  44383  snhesn  44572  unirnmapsn  45990  sge0fodjrnlem  47190  isubgr3stgrlem4  48794  usgrexmpl2trifr  48862  smprngprmrng  49163  isidom3  49169  lindslinindsimp1  49296