Theorem elsn 4607

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

Syntax hints:   ↔ wb 206   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {csn 4592

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-sn 4593

This theorem is referenced by:  velsn  4608  opthwiener  5477  brsnop  5485  opthprc  5705  dmsnn0  6183  dmsnopg  6189  cnvcnvsn  6195  snsn0non  6462  funconstss  7031  fniniseg  7035  fniniseg2  7037  fsn  7110  fconstfv  7189  eusvobj2  7382  fnse  8115  xpord2pred  8127  xpord2indlem  8129  fisn  9385  axdc3lem4  10413  axdc4lem  10415  axcclem  10417  opelreal  11090  seqid3  14018  seqz  14022  1exp  14063  hashf1lem2  14428  fprodn0f  15964  imasaddfnlem  17498  initoid  17970  termoid  17971  0subm  18751  smndex1mgm  18841  smndex1n0mnd  18846  grpinvfval  18917  0subg  19090  0subgOLD  19091  0nsg  19108  eqg0subg  19135  kerf1ghm  19186  sylow2alem2  19555  gsumval3  19844  gsumzaddlem  19858  lsssn0  20861  rngqiprngimf1  21217  pzriprnglem8  21405  r0cld  23632  alexsubALTlem2  23942  tgphaus  24011  isusp  24156  i1f1lem  25597  ig1pcl  26091  plyco0  26104  plyeq0lem  26122  plycj  26190  plycjOLD  26192  wilthlem2  26986  dchrfi  27173  mulsval  28019  snstriedgval  28972  incistruhgr  29013  1loopgrnb0  29437  umgr2v2enb1  29461  usgr2pthlem  29700  hsn0elch  31184  h1de2ctlem  31491  atomli  32318  suppiniseg  32616  1stpreimas  32636  gsummpt2d  32996  kerunit  33304  exsslsb  33599  qqhval2lem  33978  qqhf  33983  qqhre  34017  esum2dlem  34089  eulerpartlemb  34366  bnj149  34872  subfacp1lem6  35179  ellimits  35905  weiunse  36463  bj-0nel1  36948  bj-isrvec  37289  poimirlem18  37639  poimirlem21  37642  poimirlem22  37643  poimirlem31  37652  poimirlem32  37653  itg2addnclem2  37673  ftc1anclem3  37696  0idl  38026  keridl  38033  smprngopr  38053  isdmn3  38075  ellkr  39089  diblss  41171  dihmeetlem4preN  41307  dihmeetlem13N  41320  sticksstones11  42151  0prjspnrel  42622  pw2f1ocnv  43033  fvnonrel  43593  snhesn  43782  unirnmapsn  45215  sge0fodjrnlem  46421  isubgr3stgrlem4  47972  usgrexmpl2trifr  48032  lindslinindsimp1  48450