Theorem elsn 4644

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

Syntax hints:   ↔ wb 205   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4630

This theorem is referenced by:  velsn  4645  opthwiener  5515  brsnop  5523  opthprc  5741  dmsnn0  6207  dmsnopg  6213  cnvcnvsn  6219  snsn0non  6490  funconstss  7058  fniniseg  7062  fniniseg2  7064  fsn  7133  fconstfv  7214  eusvobj2  7401  fnse  8119  xpord2pred  8131  xpord2indlem  8133  wfrlem14OLD  8322  fisn  9422  axdc3lem4  10448  axdc4lem  10450  axcclem  10452  opelreal  11125  seqid3  14012  seqz  14016  1exp  14057  hashf1lem2  14417  fprodn0f  15935  imasaddfnlem  17474  initoid  17951  termoid  17952  0subm  18698  smndex1mgm  18788  smndex1n0mnd  18793  grpinvfval  18863  0subg  19031  0subgOLD  19032  0nsg  19049  eqg0subg  19073  sylow2alem2  19486  gsumval3  19775  gsumzaddlem  19789  kerf1ghm  20282  lsssn0  20558  r0cld  23242  alexsubALTlem2  23552  tgphaus  23621  isusp  23766  i1f1lem  25206  ig1pcl  25693  plyco0  25706  plyeq0lem  25724  plycj  25791  wilthlem2  26573  dchrfi  26758  mulsval  27565  snstriedgval  28298  incistruhgr  28339  1loopgrnb0  28759  umgr2v2enb1  28783  usgr2pthlem  29020  hsn0elch  30501  h1de2ctlem  30808  atomli  31635  suppiniseg  31908  1stpreimas  31927  gsummpt2d  32201  kerunit  32437  qqhval2lem  32961  qqhf  32966  qqhre  33000  esum2dlem  33090  eulerpartlemb  33367  bnj149  33886  subfacp1lem6  34176  ellimits  34882  bj-0nel1  35834  bj-isrvec  36175  poimirlem18  36506  poimirlem21  36509  poimirlem22  36510  poimirlem31  36519  poimirlem32  36520  itg2addnclem2  36540  ftc1anclem3  36563  0idl  36893  keridl  36900  smprngopr  36920  isdmn3  36942  ellkr  37959  diblss  40041  dihmeetlem4preN  40177  dihmeetlem13N  40190  sticksstones11  40972  0prjspnrel  41369  pw2f1ocnv  41776  fvnonrel  42348  snhesn  42537  unirnmapsn  43913  sge0fodjrnlem  45132  rngqiprngimf1  46785  pzriprnglem8  46812  lindslinindsimp1  47138