Theorem elsn 4663

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

Syntax hints:   ↔ wb 206   = wceq 1537   ∈ wcel 2108  Vcvv 3488  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-sn 4649

This theorem is referenced by:  velsn  4664  opthwiener  5533  brsnop  5541  opthprc  5764  dmsnn0  6238  dmsnopg  6244  cnvcnvsn  6250  snsn0non  6520  funconstss  7089  fniniseg  7093  fniniseg2  7095  fsn  7169  fconstfv  7249  eusvobj2  7440  fnse  8174  xpord2pred  8186  xpord2indlem  8188  wfrlem14OLD  8378  fisn  9496  axdc3lem4  10522  axdc4lem  10524  axcclem  10526  opelreal  11199  seqid3  14097  seqz  14101  1exp  14142  hashf1lem2  14505  fprodn0f  16039  imasaddfnlem  17588  initoid  18068  termoid  18069  0subm  18852  smndex1mgm  18942  smndex1n0mnd  18947  grpinvfval  19018  0subg  19191  0subgOLD  19192  0nsg  19209  eqg0subg  19236  kerf1ghm  19287  sylow2alem2  19660  gsumval3  19949  gsumzaddlem  19963  lsssn0  20969  rngqiprngimf1  21333  pzriprnglem8  21522  r0cld  23767  alexsubALTlem2  24077  tgphaus  24146  isusp  24291  i1f1lem  25743  ig1pcl  26238  plyco0  26251  plyeq0lem  26269  plycj  26337  wilthlem2  27130  dchrfi  27317  mulsval  28153  snstriedgval  29073  incistruhgr  29114  1loopgrnb0  29538  umgr2v2enb1  29562  usgr2pthlem  29799  hsn0elch  31280  h1de2ctlem  31587  atomli  32414  suppiniseg  32698  1stpreimas  32717  gsummpt2d  33032  kerunit  33314  qqhval2lem  33927  qqhf  33932  qqhre  33966  esum2dlem  34056  eulerpartlemb  34333  bnj149  34851  subfacp1lem6  35153  ellimits  35874  weiunse  36434  bj-0nel1  36919  bj-isrvec  37260  poimirlem18  37598  poimirlem21  37601  poimirlem22  37602  poimirlem31  37611  poimirlem32  37612  itg2addnclem2  37632  ftc1anclem3  37655  0idl  37985  keridl  37992  smprngopr  38012  isdmn3  38034  ellkr  39045  diblss  41127  dihmeetlem4preN  41263  dihmeetlem13N  41276  sticksstones11  42113  0prjspnrel  42582  pw2f1ocnv  42994  fvnonrel  43559  snhesn  43748  unirnmapsn  45121  sge0fodjrnlem  46337  usgrexmpl2trifr  47852  lindslinindsimp1  48186