Theorem elsn 4583

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3430  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4569

This theorem is referenced by:  velsn  4584  opthwiener  5463  brsnop  5471  opthprc  5689  dmsnn0  6166  dmsnopg  6172  cnvcnvsn  6178  snsn0non  6444  funconstss  7003  fniniseg  7007  fniniseg2  7009  fsn  7083  fconstfv  7161  eusvobj2  7353  fnse  8077  xpord2pred  8089  xpord2indlem  8091  fisn  9334  axdc3lem4  10369  axdc4lem  10371  axcclem  10373  opelreal  11047  seqid3  14002  seqz  14006  1exp  14047  hashf1lem2  14412  fprodn0f  15950  imasaddfnlem  17486  initoid  17962  termoid  17963  0subm  18779  smndex1mgm  18872  smndex1n0mnd  18877  grpinvfval  18948  0subg  19121  0nsg  19138  eqg0subg  19165  kerf1ghm  19216  sylow2alem2  19587  gsumval3  19876  gsumzaddlem  19890  lsssn0  20937  rngqiprngimf1  21293  pzriprnglem8  21481  r0cld  23716  alexsubALTlem2  24026  tgphaus  24095  isusp  24239  i1f1lem  25669  ig1pcl  26157  plyco0  26170  plyeq0lem  26188  plycj  26255  plycjOLD  26257  wilthlem2  27049  dchrfi  27235  mulsval  28118  snstriedgval  29124  incistruhgr  29165  1loopgrnb0  29589  umgr2v2enb1  29613  usgr2pthlem  29849  hsn0elch  31337  h1de2ctlem  31644  atomli  32471  suppiniseg  32777  1stpreimas  32797  gsummpt2d  33128  kerunit  33403  exsslsb  33759  qqhval2lem  34144  qqhf  34149  qqhre  34183  esum2dlem  34255  eulerpartlemb  34531  bnj149  35036  subfacp1lem6  35386  ellimits  36109  weiunse  36669  bj-0nel1  37279  bj-isrvec  37627  poimirlem18  37976  poimirlem21  37979  poimirlem22  37980  poimirlem31  37989  poimirlem32  37990  itg2addnclem2  38010  ftc1anclem3  38033  0idl  38363  keridl  38370  smprngopr  38390  isdmn3  38412  ellkr  39552  diblss  41633  dihmeetlem4preN  41769  dihmeetlem13N  41782  sticksstones11  42612  0prjspnrel  43077  pw2f1ocnv  43486  fvnonrel  44045  snhesn  44234  unirnmapsn  45664  sge0fodjrnlem  46865  isubgr3stgrlem4  48460  usgrexmpl2trifr  48528  lindslinindsimp1  48948