Theorem elsn 4599

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2145  Vcvv 3450  {csn 4584

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-sn 4585

This theorem is used by:  velsn  4600  opthwiener  5491  brsnop  5500  opthprc  5719  dmsnn0  6203  dmsnopg  6209  cnvcnvsn  6215  snsn0non  6484  funconstss  7049  fniniseg  7053  fniniseg2  7055  fsn  7130  fconstfv  7212  eusvobj2  7406  fnse  8132  xpord2pred  8144  xpord2indlem  8146  fisn  9398  axdc3lem4  10456  axdc4lem  10458  axcclem  10460  opelreal  11140  seqid3  14111  seqz  14115  1exp  14156  hashf1lem2  14522  fprodn0f  16079  imasaddfnlem  17615  initoid  18091  termoid  18092  0subm  18927  smndex1mgm  19020  smndex1n0mnd  19025  grpinvfval  19103  0subg  19276  0nsg  19293  eqg0subg  19325  kerf1ghm  19375  sylow2alem2  19746  gsumval3  20035  gsumzaddlem  20049  lsssn0  21133  rngqiprngimf1  21504  pzriprnglem8  21702  r0cld  23965  alexsubALTlem2  24275  tgphaus  24344  isusp  24488  i1f1lem  25918  ig1pcl  26405  plyco0  26418  plyeq0lem  26437  plycj  26504  plycjOLD  26506  wilthlem2  27306  dchrfi  27492  mulsval  28375  snstriedgval  29496  incistruhgr  29537  1loopgrnb0  29963  umgr2v2enb1  29987  usgr2pthlem  30229  hsn0elch  31730  h1de2ctlem  32037  atomli  32864  suppiniseg  33159  1stpreimas  33179  gsummpt2d  33490  kerunit  33766  exsslsb  34108  qqhval2lem  34492  qqhf  34497  qqhre  34531  esum2dlem  34603  eulerpartlemb  34880  bnj149  35385  subfacp1lem6  35765  ellimits  36488  nmulprop  36771  weiunse  37088  bj-0nel1  37698  bj-isrvec  38047  poimirlem18  38388  poimirlem21  38391  poimirlem22  38392  poimirlem31  38401  poimirlem32  38402  itg2addnclem2  38422  ftc1anclem3  38445  0idl  38776  keridl  38783  smprngopr  38803  isdmn3  38825  ellkr  39963  diblss  42044  dihmeetlem4preN  42180  dihmeetlem13N  42193  sticksstones11  43023  0prjspnrel  43474  pw2f1ocnv  43879  fvnonrel  44438  snhesn  44627  unirnmapsn  46045  sge0fodjrnlem  47245  tmachlem-agreeprod  47766  isubgr3stgrlem4  48886  usgrexmpl2trifr  48954  smprngprmrng  49255  isidom3  49261  lindslinindsimp1  49388