Theorem elsn 4604

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

Syntax hints:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-sn 4590

This theorem is referenced by:  velsn  4605  opthwiener  5497  brsnop  5506  opthprc  5725  dmsnn0  6208  dmsnopg  6214  cnvcnvsn  6220  snsn0non  6487  funconstss  7051  fniniseg  7055  fniniseg2  7057  fsn  7131  fconstfv  7210  eusvobj2  7402  fnse  8125  xpord2pred  8137  xpord2indlem  8139  fisn  9383  axdc3lem4  10432  axdc4lem  10434  axcclem  10436  opelreal  11110  seqid3  14078  seqz  14082  1exp  14123  hashf1lem2  14489  fprodn0f  16041  imasaddfnlem  17577  initoid  18053  termoid  18054  0subm  18871  smndex1mgm  18964  smndex1n0mnd  18969  grpinvfval  19040  0subg  19213  0nsg  19230  eqg0subg  19262  kerf1ghm  19312  sylow2alem2  19683  gsumval3  19972  gsumzaddlem  19986  lsssn0  21069  rngqiprngimf1  21440  pzriprnglem8  21638  r0cld  23895  alexsubALTlem2  24205  tgphaus  24274  isusp  24418  i1f1lem  25848  ig1pcl  26336  plyco0  26349  plyeq0lem  26367  plycj  26434  plycjOLD  26436  wilthlem2  27233  dchrfi  27419  mulsval  28302  snstriedgval  29388  incistruhgr  29429  1loopgrnb0  29852  umgr2v2enb1  29876  usgr2pthlem  30112  hsn0elch  31600  h1de2ctlem  31907  atomli  32734  suppiniseg  33031  1stpreimas  33051  gsummpt2d  33369  kerunit  33645  exsslsb  33987  qqhval2lem  34371  qqhf  34376  qqhre  34410  esum2dlem  34482  eulerpartlemb  34758  bnj149  35263  subfacp1lem6  35677  ellimits  36400  nmulprop  36682  weiunse  36999  bj-0nel1  37609  bj-isrvec  37958  poimirlem18  38309  poimirlem21  38312  poimirlem22  38313  poimirlem31  38322  poimirlem32  38323  itg2addnclem2  38343  ftc1anclem3  38366  0idl  38696  keridl  38703  smprngopr  38723  isdmn3  38745  ellkr  39883  diblss  41964  dihmeetlem4preN  42100  dihmeetlem13N  42113  sticksstones11  42943  0prjspnrel  43379  pw2f1ocnv  43784  fvnonrel  44343  snhesn  44532  unirnmapsn  45950  sge0fodjrnlem  47150  isubgr3stgrlem4  48754  usgrexmpl2trifr  48822  smprngprmrng  49124  isidom3  49130  lindslinindsimp1  49257