Theorem elsn 4331

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

Syntax hints:   ↔ wb 196   = wceq 1631   ∈ wcel 2145  Vcvv 3351  {csn 4316

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-sn 4317

This theorem is referenced by:  velsn  4332  opthwiener  5107  opthprc  5307  dmsnn0  5741  dmsnopg  5748  cnvcnvsn  5754  snsn0non  5989  funconstss  6478  fniniseg  6481  fniniseg2  6483  fsn  6545  fconstfv  6620  eusvobj2  6786  fnse  7445  wfrlem14  7581  mapdm0  8024  fisn  8489  axdc3lem4  9477  axdc4lem  9479  axcclem  9481  opelreal  10153  seqid3  13052  seqz  13056  1exp  13096  hashf1lem2  13442  fprodn0f  14928  imasaddfnlem  16396  initoid  16862  termoid  16863  0subg  17827  0nsg  17847  sylow2alem2  18240  gsumval3  18515  gsumzaddlem  18528  kerf1hrm  18953  lsssn0  19158  r0cld  21762  alexsubALTlem2  22072  tgphaus  22140  isusp  22285  i1f1lem  23676  ig1pcl  24155  plyco0  24168  plyeq0lem  24186  plycj  24253  wilthlem2  25016  dchrfi  25201  snstriedgval  26151  incistruhgr  26195  1loopgrnb0  26633  umgr2v2enb1  26657  usgr2pthlem  26894  hsn0elch  28445  h1de2ctlem  28754  atomli  29581  1stpreimas  29823  gsummpt2d  30121  kerunit  30163  qqhval2lem  30365  qqhf  30370  qqhre  30404  esum2dlem  30494  eulerpartlemb  30770  bnj149  31283  subfacp1lem6  31505  ellimits  32354  bj-0nel1  33271  poimirlem18  33760  poimirlem21  33763  poimirlem22  33764  poimirlem31  33773  poimirlem32  33774  itg2addnclem2  33794  ftc1anclem3  33819  0idl  34156  keridl  34163  smprngopr  34183  isdmn3  34205  ellkr  34898  diblss  36980  dihmeetlem4preN  37116  dihmeetlem13N  37129  pw2f1ocnv  38130  fvnonrel  38429  snhesn  38606  unirnmapsn  39924  sge0fodjrnlem  41150  lindslinindsimp1  42774