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 206   = wceq 1540   ∈ wcel 2109  Vcvv 3447  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-sn 4590

This theorem is referenced by:  velsn  4605  opthwiener  5474  brsnop  5482  opthprc  5702  dmsnn0  6180  dmsnopg  6186  cnvcnvsn  6192  snsn0non  6459  funconstss  7028  fniniseg  7032  fniniseg2  7034  fsn  7107  fconstfv  7186  eusvobj2  7379  fnse  8112  xpord2pred  8124  xpord2indlem  8126  fisn  9378  axdc3lem4  10406  axdc4lem  10408  axcclem  10410  opelreal  11083  seqid3  14011  seqz  14015  1exp  14056  hashf1lem2  14421  fprodn0f  15957  imasaddfnlem  17491  initoid  17963  termoid  17964  0subm  18744  smndex1mgm  18834  smndex1n0mnd  18839  grpinvfval  18910  0subg  19083  0subgOLD  19084  0nsg  19101  eqg0subg  19128  kerf1ghm  19179  sylow2alem2  19548  gsumval3  19837  gsumzaddlem  19851  lsssn0  20854  rngqiprngimf1  21210  pzriprnglem8  21398  r0cld  23625  alexsubALTlem2  23935  tgphaus  24004  isusp  24149  i1f1lem  25590  ig1pcl  26084  plyco0  26097  plyeq0lem  26115  plycj  26183  plycjOLD  26185  wilthlem2  26979  dchrfi  27166  mulsval  28012  snstriedgval  28965  incistruhgr  29006  1loopgrnb0  29430  umgr2v2enb1  29454  usgr2pthlem  29693  hsn0elch  31177  h1de2ctlem  31484  atomli  32311  suppiniseg  32609  1stpreimas  32629  gsummpt2d  32989  kerunit  33297  exsslsb  33592  qqhval2lem  33971  qqhf  33976  qqhre  34010  esum2dlem  34082  eulerpartlemb  34359  bnj149  34865  subfacp1lem6  35172  ellimits  35898  weiunse  36456  bj-0nel1  36941  bj-isrvec  37282  poimirlem18  37632  poimirlem21  37635  poimirlem22  37636  poimirlem31  37645  poimirlem32  37646  itg2addnclem2  37666  ftc1anclem3  37689  0idl  38019  keridl  38026  smprngopr  38046  isdmn3  38068  ellkr  39082  diblss  41164  dihmeetlem4preN  41300  dihmeetlem13N  41313  sticksstones11  42144  0prjspnrel  42615  pw2f1ocnv  43026  fvnonrel  43586  snhesn  43775  unirnmapsn  45208  sge0fodjrnlem  46414  isubgr3stgrlem4  47968  usgrexmpl2trifr  48028  lindslinindsimp1  48446