Theorem elsn 4593

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

Syntax hints:   ↔ wb 206   = wceq 1541   ∈ wcel 2113  Vcvv 3438  {csn 4578

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 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-sn 4579

This theorem is referenced by:  velsn  4594  opthwiener  5460  brsnop  5468  opthprc  5686  dmsnn0  6163  dmsnopg  6169  cnvcnvsn  6175  snsn0non  6441  funconstss  6999  fniniseg  7003  fniniseg2  7005  fsn  7078  fconstfv  7156  eusvobj2  7348  fnse  8073  xpord2pred  8085  xpord2indlem  8087  fisn  9328  axdc3lem4  10361  axdc4lem  10363  axcclem  10365  opelreal  11039  seqid3  13967  seqz  13971  1exp  14012  hashf1lem2  14377  fprodn0f  15912  imasaddfnlem  17447  initoid  17923  termoid  17924  0subm  18740  smndex1mgm  18830  smndex1n0mnd  18835  grpinvfval  18906  0subg  19079  0nsg  19096  eqg0subg  19123  kerf1ghm  19174  sylow2alem2  19545  gsumval3  19834  gsumzaddlem  19848  lsssn0  20897  rngqiprngimf1  21253  pzriprnglem8  21441  r0cld  23680  alexsubALTlem2  23990  tgphaus  24059  isusp  24203  i1f1lem  25644  ig1pcl  26138  plyco0  26151  plyeq0lem  26169  plycj  26237  plycjOLD  26239  wilthlem2  27033  dchrfi  27220  mulsval  28078  snstriedgval  29060  incistruhgr  29101  1loopgrnb0  29525  umgr2v2enb1  29549  usgr2pthlem  29785  hsn0elch  31272  h1de2ctlem  31579  atomli  32406  suppiniseg  32714  1stpreimas  32734  gsummpt2d  33081  kerunit  33355  exsslsb  33702  qqhval2lem  34087  qqhf  34092  qqhre  34126  esum2dlem  34198  eulerpartlemb  34474  bnj149  34980  subfacp1lem6  35328  ellimits  36051  weiunse  36611  bj-0nel1  37097  bj-isrvec  37438  poimirlem18  37778  poimirlem21  37781  poimirlem22  37782  poimirlem31  37791  poimirlem32  37792  itg2addnclem2  37812  ftc1anclem3  37835  0idl  38165  keridl  38172  smprngopr  38192  isdmn3  38214  ellkr  39288  diblss  41369  dihmeetlem4preN  41505  dihmeetlem13N  41518  sticksstones11  42349  0prjspnrel  42812  pw2f1ocnv  43221  fvnonrel  43780  snhesn  43969  unirnmapsn  45400  sge0fodjrnlem  46602  isubgr3stgrlem4  48157  usgrexmpl2trifr  48225  lindslinindsimp1  48645