Theorem elsn 4599

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

This proof depends on syntax axioms:   ↔ wb 209   = wceq 1570   ∈ wcel 2147  Vcvv 3454  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-sn 4589

This theorem is used by:  velsn  4600  opthwiener  5494  brsnop  5503  opthprc  5722  dmsnn0  6227  dmsnopg  6233  cnvcnvsn  6239  snsn0non  6515  funconstss  7086  fniniseg  7091  fniniseg2  7093  fsn  7168  fconstfv  7249  eusvobj2  7443  fnse  8187  xpord2pred  8199  xpord2indlem  8201  fisn  9456  axdc3lem4  10570  axdc4lem  10572  axcclem  10574  opelreal  11254  seqid3  14229  seqz  14233  1exp  14274  hashf1lem2  14642  fprodn0f  16202  imasaddfnlem  17750  initoid  18226  termoid  18227  0subm  19063  smndex1mgm  19156  smndex1n0mnd  19161  grpinvfval  19239  0subg  19412  0nsg  19429  eqg0subg  19461  kerf1ghm  19511  sylow2alem2  19883  gsumval3  20172  gsumzaddlem  20186  lsssn0  21274  rngqiprngimf1  21647  pzriprnglem8  21849  r0cld  24112  alexsubALTlem2  24422  tgphaus  24491  isusp  24635  i1f1lem  26065  ig1pcl  26552  plyco0  26565  plyeq0lem  26584  plycj  26651  wilthlem2  27453  dchrfi  27639  mulsval  28552  snstriedgval  29673  incistruhgr  29714  1loopgrnb0  30140  umgr2v2enb1  30164  usgr2pthlem  30406  hsn0elch  31907  h1de2ctlem  32214  atomli  33041  suppiniseg  33376  1stpreimas  33396  gsummpt2d  33709  kerunit  33990  exsslsb  34340  qqhval2lem  34724  qqhf  34729  qqhre  34763  esum2dlem  34835  eulerpartlemb  35111  bnj149  35616  subfacp1lem6  36158  ellimits  36887  nmulprop  37154  weiunse  37471  bj-0nel1  38081  bj-isrvec  38483  poimirlem18  38824  poimirlem21  38827  poimirlem22  38828  poimirlem31  38837  poimirlem32  38838  itg2addnclem2  38858  ftc1anclem3  38881  0idl  39225  keridl  39232  smprngopr  39252  isdmn3  39274  ellkr  40412  diblss  42493  dihmeetlem4preN  42629  dihmeetlem13N  42642  sticksstones11  43472  0prjspnrel  43929  pw2f1ocnv  44310  fvnonrel  44858  snhesn  45047  unirnmapsn  46500  sge0fodjrnlem  47699  tmachlem-agreeprod  48220  isubgr3stgrlem4  49340  usgrexmpl2trifr  49408  smprngprmrng  49767  isidom3  49773  lindslinindsimp1  49900