Theorem elsn 4597

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

Syntax hints:   ↔ wb 206   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-sn 4583

This theorem is referenced by:  velsn  4598  opthwiener  5470  brsnop  5478  opthprc  5696  dmsnn0  6173  dmsnopg  6179  cnvcnvsn  6185  snsn0non  6451  funconstss  7010  fniniseg  7014  fniniseg2  7016  fsn  7090  fconstfv  7168  eusvobj2  7360  fnse  8085  xpord2pred  8097  xpord2indlem  8099  fisn  9342  axdc3lem4  10375  axdc4lem  10377  axcclem  10379  opelreal  11053  seqid3  13981  seqz  13985  1exp  14026  hashf1lem2  14391  fprodn0f  15926  imasaddfnlem  17461  initoid  17937  termoid  17938  0subm  18754  smndex1mgm  18844  smndex1n0mnd  18849  grpinvfval  18920  0subg  19093  0nsg  19110  eqg0subg  19137  kerf1ghm  19188  sylow2alem2  19559  gsumval3  19848  gsumzaddlem  19862  lsssn0  20911  rngqiprngimf1  21267  pzriprnglem8  21455  r0cld  23694  alexsubALTlem2  24004  tgphaus  24073  isusp  24217  i1f1lem  25658  ig1pcl  26152  plyco0  26165  plyeq0lem  26183  plycj  26251  plycjOLD  26253  wilthlem2  27047  dchrfi  27234  mulsval  28117  snstriedgval  29123  incistruhgr  29164  1loopgrnb0  29588  umgr2v2enb1  29612  usgr2pthlem  29848  hsn0elch  31336  h1de2ctlem  31643  atomli  32470  suppiniseg  32776  1stpreimas  32796  gsummpt2d  33143  kerunit  33418  exsslsb  33774  qqhval2lem  34159  qqhf  34164  qqhre  34198  esum2dlem  34270  eulerpartlemb  34546  bnj149  35051  subfacp1lem6  35401  ellimits  36124  weiunse  36684  bj-0nel1  37201  bj-isrvec  37549  poimirlem18  37889  poimirlem21  37892  poimirlem22  37893  poimirlem31  37902  poimirlem32  37903  itg2addnclem2  37923  ftc1anclem3  37946  0idl  38276  keridl  38283  smprngopr  38303  isdmn3  38325  ellkr  39465  diblss  41546  dihmeetlem4preN  41682  dihmeetlem13N  41695  sticksstones11  42526  0prjspnrel  42985  pw2f1ocnv  43394  fvnonrel  43953  snhesn  44142  unirnmapsn  45572  sge0fodjrnlem  46774  isubgr3stgrlem4  48329  usgrexmpl2trifr  48397  lindslinindsimp1  48817