Theorem elsn 4643

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

Syntax hints:   ↔ wb 205   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {csn 4628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-sn 4629

This theorem is referenced by:  velsn  4644  opthwiener  5514  brsnop  5522  opthprc  5740  dmsnn0  6206  dmsnopg  6212  cnvcnvsn  6218  snsn0non  6489  funconstss  7057  fniniseg  7061  fniniseg2  7063  fsn  7132  fconstfv  7213  eusvobj2  7400  fnse  8118  xpord2pred  8130  xpord2indlem  8132  wfrlem14OLD  8321  fisn  9421  axdc3lem4  10447  axdc4lem  10449  axcclem  10451  opelreal  11124  seqid3  14011  seqz  14015  1exp  14056  hashf1lem2  14416  fprodn0f  15934  imasaddfnlem  17473  initoid  17950  termoid  17951  0subm  18697  smndex1mgm  18787  smndex1n0mnd  18792  grpinvfval  18862  0subg  19030  0subgOLD  19031  0nsg  19048  eqg0subg  19072  sylow2alem2  19485  gsumval3  19774  gsumzaddlem  19788  kerf1ghm  20281  lsssn0  20557  r0cld  23241  alexsubALTlem2  23551  tgphaus  23620  isusp  23765  i1f1lem  25205  ig1pcl  25692  plyco0  25705  plyeq0lem  25723  plycj  25790  wilthlem2  26570  dchrfi  26755  mulsval  27562  snstriedgval  28295  incistruhgr  28336  1loopgrnb0  28756  umgr2v2enb1  28780  usgr2pthlem  29017  hsn0elch  30496  h1de2ctlem  30803  atomli  31630  suppiniseg  31903  1stpreimas  31922  gsummpt2d  32196  kerunit  32432  qqhval2lem  32956  qqhf  32961  qqhre  32995  esum2dlem  33085  eulerpartlemb  33362  bnj149  33881  subfacp1lem6  34171  ellimits  34877  bj-0nel1  35829  bj-isrvec  36170  poimirlem18  36501  poimirlem21  36504  poimirlem22  36505  poimirlem31  36514  poimirlem32  36515  itg2addnclem2  36535  ftc1anclem3  36558  0idl  36888  keridl  36895  smprngopr  36915  isdmn3  36937  ellkr  37954  diblss  40036  dihmeetlem4preN  40172  dihmeetlem13N  40185  sticksstones11  40967  0prjspnrel  41370  pw2f1ocnv  41766  fvnonrel  42338  snhesn  42527  unirnmapsn  43903  sge0fodjrnlem  45122  rngqiprngimf1  46775  pzriprnglem8  46802  lindslinindsimp1  47128