Theorem elsn 4609

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

Syntax hints:   ↔ wb 209   = wceq 1567   ∈ wcel 2149  Vcvv 3463  {csn 4594

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-sn 4595

This theorem is referenced by:  velsn  4610  opthwiener  5498  brsnop  5507  opthprc  5726  dmsnn0  6209  dmsnopg  6215  cnvcnvsn  6221  snsn0non  6488  funconstss  7052  fniniseg  7056  fniniseg2  7058  fsn  7132  fconstfv  7211  eusvobj2  7403  fnse  8129  xpord2pred  8141  xpord2indlem  8143  fisn  9387  axdc3lem4  10437  axdc4lem  10439  axcclem  10441  opelreal  11115  seqid3  14082  seqz  14086  1exp  14127  hashf1lem2  14493  fprodn0f  16045  imasaddfnlem  17582  initoid  18058  termoid  18059  0subm  18876  smndex1mgm  18969  smndex1n0mnd  18974  grpinvfval  19045  0subg  19218  0nsg  19235  eqg0subg  19267  kerf1ghm  19317  sylow2alem2  19688  gsumval3  19977  gsumzaddlem  19991  lsssn0  21047  rngqiprngimf1  21411  pzriprnglem8  21607  r0cld  23864  alexsubALTlem2  24174  tgphaus  24243  isusp  24387  i1f1lem  25817  ig1pcl  26305  plyco0  26318  plyeq0lem  26336  plycj  26403  plycjOLD  26405  wilthlem2  27199  dchrfi  27385  mulsval  28268  snstriedgval  29329  incistruhgr  29370  1loopgrnb0  29793  umgr2v2enb1  29817  usgr2pthlem  30053  hsn0elch  31541  h1de2ctlem  31848  atomli  32675  suppiniseg  32972  1stpreimas  32992  gsummpt2d  33310  kerunit  33588  exsslsb  33932  qqhval2lem  34316  qqhf  34321  qqhre  34355  esum2dlem  34427  eulerpartlemb  34703  bnj149  35208  subfacp1lem6  35576  ellimits  36299  nmulprop  36581  weiunse  36868  bj-0nel1  37477  bj-isrvec  37826  poimirlem18  38177  poimirlem21  38180  poimirlem22  38181  poimirlem31  38190  poimirlem32  38191  itg2addnclem2  38211  ftc1anclem3  38234  0idl  38564  keridl  38571  smprngopr  38591  isdmn3  38613  ellkr  39753  diblss  41834  dihmeetlem4preN  41970  dihmeetlem13N  41983  sticksstones11  42813  0prjspnrel  43251  pw2f1ocnv  43656  fvnonrel  44215  snhesn  44404  unirnmapsn  45822  sge0fodjrnlem  47022  isubgr3stgrlem4  48623  usgrexmpl2trifr  48691  smprngprmrng  48993  lindslinindsimp1  49122