Theorem elsn 4598

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1569   ∈ wcel 2146  Vcvv 3453  {csn 4587

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4588

This theorem is used by:  velsn  4599  opthwiener  5490  brsnop  5499  opthprc  5718  dmsnn0  6214  dmsnopg  6220  cnvcnvsn  6226  snsn0non  6495  funconstss  7063  fniniseg  7067  fniniseg2  7069  fsn  7144  fconstfv  7225  eusvobj2  7419  fnse  8160  xpord2pred  8172  xpord2indlem  8174  fisn  9429  axdc3lem4  10541  axdc4lem  10543  axcclem  10545  opelreal  11225  seqid3  14199  seqz  14203  1exp  14244  hashf1lem2  14611  fprodn0f  16170  imasaddfnlem  17712  initoid  18188  termoid  18189  0subm  19025  smndex1mgm  19118  smndex1n0mnd  19123  grpinvfval  19201  0subg  19374  0nsg  19391  eqg0subg  19423  kerf1ghm  19473  sylow2alem2  19844  gsumval3  20133  gsumzaddlem  20147  lsssn0  21235  rngqiprngimf1  21608  pzriprnglem8  21806  r0cld  24069  alexsubALTlem2  24379  tgphaus  24448  isusp  24592  i1f1lem  26022  ig1pcl  26509  plyco0  26522  plyeq0lem  26541  plycj  26608  wilthlem2  27408  dchrfi  27594  mulsval  28507  snstriedgval  29628  incistruhgr  29669  1loopgrnb0  30095  umgr2v2enb1  30119  usgr2pthlem  30361  hsn0elch  31862  h1de2ctlem  32169  atomli  32996  suppiniseg  33333  1stpreimas  33353  gsummpt2d  33663  kerunit  33939  exsslsb  34282  qqhval2lem  34666  qqhf  34671  qqhre  34705  esum2dlem  34777  eulerpartlemb  35053  bnj149  35558  subfacp1lem6  36071  ellimits  36799  nmulprop  37066  weiunse  37383  bj-0nel1  37993  bj-isrvec  38355  poimirlem18  38696  poimirlem21  38699  poimirlem22  38700  poimirlem31  38709  poimirlem32  38710  itg2addnclem2  38730  ftc1anclem3  38753  0idl  39099  keridl  39106  smprngopr  39126  isdmn3  39148  ellkr  40286  diblss  42367  dihmeetlem4preN  42503  dihmeetlem13N  42516  sticksstones11  43346  0prjspnrel  43803  pw2f1ocnv  44184  fvnonrel  44737  snhesn  44926  unirnmapsn  46366  sge0fodjrnlem  47565  tmachlem-agreeprod  48086  isubgr3stgrlem4  49206  usgrexmpl2trifr  49274  smprngprmrng  49575  isidom3  49581  lindslinindsimp1  49708