Theorem elsn 4588

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2111  Vcvv 3436  {csn 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-sn 4574

This theorem is referenced by:  velsn  4589  opthwiener  5452  brsnop  5460  opthprc  5678  dmsnn0  6154  dmsnopg  6160  cnvcnvsn  6166  snsn0non  6432  funconstss  6989  fniniseg  6993  fniniseg2  6995  fsn  7068  fconstfv  7146  eusvobj2  7338  fnse  8063  xpord2pred  8075  xpord2indlem  8077  fisn  9311  axdc3lem4  10344  axdc4lem  10346  axcclem  10348  opelreal  11021  seqid3  13953  seqz  13957  1exp  13998  hashf1lem2  14363  fprodn0f  15898  imasaddfnlem  17432  initoid  17908  termoid  17909  0subm  18725  smndex1mgm  18815  smndex1n0mnd  18820  grpinvfval  18891  0subg  19064  0nsg  19081  eqg0subg  19108  kerf1ghm  19159  sylow2alem2  19530  gsumval3  19819  gsumzaddlem  19833  lsssn0  20881  rngqiprngimf1  21237  pzriprnglem8  21425  r0cld  23653  alexsubALTlem2  23963  tgphaus  24032  isusp  24176  i1f1lem  25617  ig1pcl  26111  plyco0  26124  plyeq0lem  26142  plycj  26210  plycjOLD  26212  wilthlem2  27006  dchrfi  27193  mulsval  28048  snstriedgval  29016  incistruhgr  29057  1loopgrnb0  29481  umgr2v2enb1  29505  usgr2pthlem  29741  hsn0elch  31228  h1de2ctlem  31535  atomli  32362  suppiniseg  32667  1stpreimas  32687  gsummpt2d  33029  kerunit  33290  exsslsb  33609  qqhval2lem  33994  qqhf  33999  qqhre  34033  esum2dlem  34105  eulerpartlemb  34381  bnj149  34887  subfacp1lem6  35229  ellimits  35952  weiunse  36512  bj-0nel1  36997  bj-isrvec  37338  poimirlem18  37688  poimirlem21  37691  poimirlem22  37692  poimirlem31  37701  poimirlem32  37702  itg2addnclem2  37722  ftc1anclem3  37745  0idl  38075  keridl  38082  smprngopr  38102  isdmn3  38124  ellkr  39198  diblss  41279  dihmeetlem4preN  41415  dihmeetlem13N  41428  sticksstones11  42259  0prjspnrel  42730  pw2f1ocnv  43140  fvnonrel  43700  snhesn  43889  unirnmapsn  45321  sge0fodjrnlem  46524  isubgr3stgrlem4  48079  usgrexmpl2trifr  48147  lindslinindsimp1  48568