Theorem elsn 4582

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

Syntax hints:   ↔ wb 208   = wceq 1537   ∈ wcel 2114  Vcvv 3494  {csn 4567

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-sn 4568

This theorem is referenced by:  velsn  4583  opthwiener  5404  opthprc  5616  dmsnn0  6064  dmsnopg  6070  cnvcnvsn  6076  snsn0non  6309  funconstss  6826  fniniseg  6830  fniniseg2  6832  fsn  6897  fconstfv  6975  eusvobj2  7149  fnse  7827  wfrlem14  7968  fisn  8891  axdc3lem4  9875  axdc4lem  9877  axcclem  9879  opelreal  10552  seqid3  13415  seqz  13419  1exp  13459  hashf1lem2  13815  fprodn0f  15345  imasaddfnlem  16801  initoid  17265  termoid  17266  0subm  17982  smndex1mgm  18072  smndex1n0mnd  18077  grpinvfval  18142  0subg  18304  0nsg  18321  sylow2alem2  18743  gsumval3  19027  gsumzaddlem  19041  kerf1ghm  19497  kerf1hrmOLD  19498  lsssn0  19719  r0cld  22346  alexsubALTlem2  22656  tgphaus  22725  isusp  22870  i1f1lem  24290  ig1pcl  24769  plyco0  24782  plyeq0lem  24800  plycj  24867  wilthlem2  25646  dchrfi  25831  snstriedgval  26823  incistruhgr  26864  1loopgrnb0  27284  umgr2v2enb1  27308  usgr2pthlem  27544  hsn0elch  29025  h1de2ctlem  29332  atomli  30159  brsnop  30429  1stpreimas  30441  gsummpt2d  30687  kerunit  30896  qqhval2lem  31222  qqhf  31227  qqhre  31261  esum2dlem  31351  eulerpartlemb  31626  bnj149  32147  subfacp1lem6  32432  ellimits  33371  bj-0nel1  34268  bj-isrvec  34578  poimirlem18  34925  poimirlem21  34928  poimirlem22  34929  poimirlem31  34938  poimirlem32  34939  itg2addnclem2  34959  ftc1anclem3  34984  0idl  35318  keridl  35325  smprngopr  35345  isdmn3  35367  ellkr  36240  diblss  38321  dihmeetlem4preN  38457  dihmeetlem13N  38470  0prjspnrel  39289  pw2f1ocnv  39654  fvnonrel  39977  snhesn  40152  unirnmapsn  41497  sge0fodjrnlem  42718  lindslinindsimp1  44532