Theorem elsn 4192

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

Syntax hints:   ↔ wb 196   = wceq 1483   ∈ wcel 1990  Vcvv 3200  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-sn 4178

This theorem is referenced by:  velsn  4193  opthwiener  4976  opthprc  5167  dmsnn0  5600  dmsnopg  5606  cnvcnvsn  5612  snsn0non  5846  funconstss  6335  fniniseg  6338  fniniseg2  6340  fsn  6402  fconstfv  6476  eusvobj2  6643  fnse  7294  wfrlem14  7428  mapdm0  7872  fisn  8333  axdc3lem4  9275  axdc4lem  9277  axcclem  9279  opelreal  9951  seqid3  12845  seqz  12849  1exp  12889  hashf1lem2  13240  fprodn0f  14722  imasaddfnlem  16188  initoid  16655  termoid  16656  0subg  17619  0nsg  17639  sylow2alem2  18033  gsumval3  18308  gsumzaddlem  18321  kerf1hrm  18743  lsssn0  18948  r0cld  21541  alexsubALTlem2  21852  tgphaus  21920  isusp  22065  i1f1lem  23456  ig1pcl  23935  plyco0  23948  plyeq0lem  23966  plycj  24033  wilthlem2  24795  dchrfi  24980  snstriedgval  25930  incistruhgr  25974  1loopgrnb0  26398  umgr2v2enb1  26422  usgr2pthlem  26659  hsn0elch  28105  h1de2ctlem  28414  atomli  29241  1stpreimas  29483  gsummpt2d  29781  kerunit  29823  qqhval2lem  30025  qqhf  30030  qqhre  30064  esum2dlem  30154  eulerpartlemb  30430  bnj149  30945  subfacp1lem6  31167  ellimits  32017  bj-0nel1  32940  poimirlem18  33427  poimirlem21  33430  poimirlem22  33431  poimirlem31  33440  poimirlem32  33441  itg2addnclem2  33462  ftc1anclem3  33487  0idl  33824  keridl  33831  smprngopr  33851  isdmn3  33873  ellkr  34376  diblss  36459  dihmeetlem4preN  36595  dihmeetlem13N  36608  pw2f1ocnv  37604  fvnonrel  37903  snhesn  38080  unirnmapsn  39406  sge0fodjrnlem  40633  lindslinindsimp1  42246