Theorem elsn 4582

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3429  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-sn 4568

This theorem is referenced by:  velsn  4583  opthwiener  5468  brsnop  5477  opthprc  5695  dmsnn0  6171  dmsnopg  6177  cnvcnvsn  6183  snsn0non  6449  funconstss  7008  fniniseg  7012  fniniseg2  7014  fsn  7088  fconstfv  7167  eusvobj2  7359  fnse  8083  xpord2pred  8095  xpord2indlem  8097  fisn  9340  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  opelreal  11053  seqid3  14008  seqz  14012  1exp  14053  hashf1lem2  14418  fprodn0f  15956  imasaddfnlem  17492  initoid  17968  termoid  17969  0subm  18785  smndex1mgm  18878  smndex1n0mnd  18883  grpinvfval  18954  0subg  19127  0nsg  19144  eqg0subg  19171  kerf1ghm  19222  sylow2alem2  19593  gsumval3  19882  gsumzaddlem  19896  lsssn0  20943  rngqiprngimf1  21298  pzriprnglem8  21468  r0cld  23703  alexsubALTlem2  24013  tgphaus  24082  isusp  24226  i1f1lem  25656  ig1pcl  26144  plyco0  26157  plyeq0lem  26175  plycj  26242  plycjOLD  26244  wilthlem2  27032  dchrfi  27218  mulsval  28101  snstriedgval  29107  incistruhgr  29148  1loopgrnb0  29571  umgr2v2enb1  29595  usgr2pthlem  29831  hsn0elch  31319  h1de2ctlem  31626  atomli  32453  suppiniseg  32759  1stpreimas  32779  gsummpt2d  33110  kerunit  33385  exsslsb  33741  qqhval2lem  34125  qqhf  34130  qqhre  34164  esum2dlem  34236  eulerpartlemb  34512  bnj149  35017  subfacp1lem6  35367  ellimits  36090  weiunse  36650  bj-0nel1  37260  bj-isrvec  37608  poimirlem18  37959  poimirlem21  37962  poimirlem22  37963  poimirlem31  37972  poimirlem32  37973  itg2addnclem2  37993  ftc1anclem3  38016  0idl  38346  keridl  38353  smprngopr  38373  isdmn3  38395  ellkr  39535  diblss  41616  dihmeetlem4preN  41752  dihmeetlem13N  41765  sticksstones11  42595  0prjspnrel  43060  pw2f1ocnv  43465  fvnonrel  44024  snhesn  44213  unirnmapsn  45643  sge0fodjrnlem  46844  isubgr3stgrlem4  48445  usgrexmpl2trifr  48513  lindslinindsimp1  48933