Theorem elsn 4225

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

Syntax hints:   ↔ wb 196   = wceq 1523   ∈ wcel 2030  Vcvv 3231  {csn 4210

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-sn 4211

This theorem is referenced by:  velsn  4226  opthwiener  5005  opthprc  5201  dmsnn0  5635  dmsnopg  5642  cnvcnvsn  5648  snsn0non  5884  funconstss  6375  fniniseg  6378  fniniseg2  6380  fsn  6442  fconstfv  6517  eusvobj2  6683  fnse  7339  wfrlem14  7473  mapdm0  7914  fisn  8374  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  opelreal  9989  seqid3  12885  seqz  12889  1exp  12929  hashf1lem2  13278  fprodn0f  14766  imasaddfnlem  16235  initoid  16702  termoid  16703  0subg  17666  0nsg  17686  sylow2alem2  18079  gsumval3  18354  gsumzaddlem  18367  kerf1hrm  18791  lsssn0  18996  r0cld  21589  alexsubALTlem2  21899  tgphaus  21967  isusp  22112  i1f1lem  23501  ig1pcl  23980  plyco0  23993  plyeq0lem  24011  plycj  24078  wilthlem2  24840  dchrfi  25025  snstriedgval  25975  incistruhgr  26019  1loopgrnb0  26454  umgr2v2enb1  26478  usgr2pthlem  26715  hsn0elch  28233  h1de2ctlem  28542  atomli  29369  1stpreimas  29611  gsummpt2d  29909  kerunit  29951  qqhval2lem  30153  qqhf  30158  qqhre  30192  esum2dlem  30282  eulerpartlemb  30558  bnj149  31071  subfacp1lem6  31293  ellimits  32142  bj-0nel1  33065  poimirlem18  33557  poimirlem21  33560  poimirlem22  33561  poimirlem31  33570  poimirlem32  33571  itg2addnclem2  33592  ftc1anclem3  33617  0idl  33954  keridl  33961  smprngopr  33981  isdmn3  34003  ellkr  34694  diblss  36776  dihmeetlem4preN  36912  dihmeetlem13N  36925  pw2f1ocnv  37921  fvnonrel  38220  snhesn  38397  unirnmapsn  39720  sge0fodjrnlem  40951  lindslinindsimp1  42571