Theorem elsn 4489

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

Syntax hints:   ↔ wb 207   = wceq 1522   ∈ wcel 2080  Vcvv 3436  {csn 4474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1778  ax-4 1792  ax-5 1889  ax-6 1948  ax-7 1993  ax-8 2082  ax-9 2090  ax-10 2111  ax-11 2125  ax-12 2140  ax-ext 2768

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1763  df-nf 1767  df-sb 2042  df-clab 2775  df-cleq 2787  df-clel 2862  df-nfc 2934  df-sn 4475

This theorem is referenced by:  velsn  4490  opthwiener  5298  opthprc  5505  dmsnn0  5942  dmsnopg  5948  cnvcnvsn  5954  snsn0non  6187  funconstss  6694  fniniseg  6698  fniniseg2  6700  fsn  6763  fconstfv  6844  eusvobj2  7012  fnse  7683  wfrlem14  7823  fisn  8740  axdc3lem4  9724  axdc4lem  9726  axcclem  9728  opelreal  10401  seqid3  13264  seqz  13268  1exp  13308  hashf1lem2  13662  fprodn0f  15178  imasaddfnlem  16630  initoid  17094  termoid  17095  grpinvfval  17899  0subg  18058  0nsg  18078  sylow2alem2  18473  gsumval3  18748  gsumzaddlem  18761  kerf1ghm  19187  kerf1hrmOLD  19188  lsssn0  19409  r0cld  22030  alexsubALTlem2  22340  tgphaus  22408  isusp  22553  i1f1lem  23973  ig1pcl  24452  plyco0  24465  plyeq0lem  24483  plycj  24550  wilthlem2  25328  dchrfi  25513  snstriedgval  26506  incistruhgr  26547  1loopgrnb0  26967  umgr2v2enb1  26991  usgr2pthlem  27226  hsn0elch  28708  h1de2ctlem  29015  atomli  29842  brsnop  30109  1stpreimas  30121  gsummpt2d  30488  kerunit  30542  qqhval2lem  30831  qqhf  30836  qqhre  30870  esum2dlem  30960  eulerpartlemb  31235  bnj149  31755  subfacp1lem6  32034  ellimits  32974  bj-0nel1  33834  poimirlem18  34454  poimirlem21  34457  poimirlem22  34458  poimirlem31  34467  poimirlem32  34468  itg2addnclem2  34488  ftc1anclem3  34513  0idl  34848  keridl  34855  smprngopr  34875  isdmn3  34897  ellkr  35769  diblss  37850  dihmeetlem4preN  37986  dihmeetlem13N  37999  0prjspnrel  38779  pw2f1ocnv  39132  fvnonrel  39455  snhesn  39630  unirnmapsn  41030  sge0fodjrnlem  42254  lindslinindsimp1  44006