Theorem elsn 4140

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

Syntax hints:   ↔ wb 195   = wceq 1475   ∈ wcel 1977  Vcvv 3173  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126

This theorem is referenced by:  velsn  4141  opthwiener  4901  opthprc  5089  dmsnn0  5518  dmsnopg  5524  cnvcnvsn  5530  snsn0non  5763  funconstss  6243  fniniseg  6246  fniniseg2  6248  fsn  6308  fconstfv  6381  eusvobj2  6542  fnse  7181  wfrlem14  7315  fisn  8216  axdc3lem4  9158  axdc4lem  9160  axcclem  9162  opelreal  9830  seqid3  12707  seqz  12711  1exp  12751  hashf1lem2  13097  fprodn0f  14561  imasaddfnlem  16011  initoid  16478  termoid  16479  0subg  17442  0nsg  17462  sylow2alem2  17856  gsumval3  18131  gsumzaddlem  18144  kerf1hrm  18566  lsssn0  18769  r0cld  21351  alexsubALTlem2  21662  tgphaus  21730  isusp  21875  i1f1lem  23262  ig1pcl  23739  plyco0  23752  plyeq0lem  23770  plycj  23837  wilthlem2  24595  dchrfi  24780  snstriedgval  25713  incistruhgr  25746  hsn0elch  27489  h1de2ctlem  27798  atomli  28625  1stpreimas  28866  gsummpt2d  29112  kerunit  29154  qqhval2lem  29353  qqhf  29358  qqhre  29392  esum2dlem  29481  eulerpartlemb  29757  bnj149  30199  subfacp1lem6  30421  ellimits  31187  bj-0nel1  32133  poimirlem18  32597  poimirlem21  32600  poimirlem22  32601  poimirlem31  32610  poimirlem32  32611  itg2addnclem2  32632  ftc1anclem3  32657  0idl  32994  keridl  33001  smprngopr  33021  isdmn3  33043  ellkr  33394  diblss  35477  dihmeetlem4preN  35613  dihmeetlem13N  35626  pw2f1ocnv  36622  fvnonrel  36922  snhesn  37100  unirnmapsn  38401  sge0fodjrnlem  39309  1loopgrnb0  40717  umgr2v2enb1  40742  usgr2pthlem  40969  lindslinindsimp1  42040