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 ⊢ (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2143  Vcvv 3455  {csn 4589

This proof depends on 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 proof 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 used 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  10441  axdc4lem  10443  axcclem  10445  opelreal  11119  seqid3  14087  seqz  14091  1exp  14132  hashf1lem2  14498  fprodn0f  16050  imasaddfnlem  17586  initoid  18062  termoid  18063  0subm  18880  smndex1mgm  18973  smndex1n0mnd  18978  grpinvfval  19049  0subg  19222  0nsg  19239  eqg0subg  19271  kerf1ghm  19321  sylow2alem2  19692  gsumval3  19981  gsumzaddlem  19995  lsssn0  21078  rngqiprngimf1  21449  pzriprnglem8  21647  r0cld  23904  alexsubALTlem2  24214  tgphaus  24283  isusp  24427  i1f1lem  25857  ig1pcl  26345  plyco0  26358  plyeq0lem  26376  plycj  26443  plycjOLD  26445  wilthlem2  27242  dchrfi  27428  mulsval  28311  snstriedgval  29397  incistruhgr  29438  1loopgrnb0  29861  umgr2v2enb1  29885  usgr2pthlem  30121  hsn0elch  31609  h1de2ctlem  31916  atomli  32743  suppiniseg  33040  1stpreimas  33060  gsummpt2d  33378  kerunit  33654  exsslsb  33996  qqhval2lem  34380  qqhf  34385  qqhre  34419  esum2dlem  34491  eulerpartlemb  34767  bnj149  35272  subfacp1lem6  35685  ellimits  36408  nmulprop  36690  weiunse  37007  bj-0nel1  37617  bj-isrvec  37966  poimirlem18  38317  poimirlem21  38320  poimirlem22  38321  poimirlem31  38330  poimirlem32  38331  itg2addnclem2  38351  ftc1anclem3  38374  0idl  38704  keridl  38711  smprngopr  38731  isdmn3  38753  ellkr  39891  diblss  41972  dihmeetlem4preN  42108  dihmeetlem13N  42121  sticksstones11  42951  0prjspnrel  43387  pw2f1ocnv  43792  fvnonrel  44351  snhesn  44540  unirnmapsn  45958  sge0fodjrnlem  47158  isubgr3stgrlem4  48762  usgrexmpl2trifr  48830  smprngprmrng  49132  isidom3  49138  lindslinindsimp1  49265