Theorem elsn 4570

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

Syntax hints:   ↔ wb 207   = wceq 1547   ∈ wcel 2119  Vcvv 3431  {csn 4555

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-sn 4556

This theorem is referenced by:  velsn  4571  opthwiener  5455  brsnop  5464  opthprc  5682  dmsnn0  6158  dmsnopg  6164  cnvcnvsn  6170  snsn0non  6436  funconstss  6997  fniniseg  7001  fniniseg2  7003  fsn  7077  fconstfv  7156  eusvobj2  7348  fnse  8073  xpord2pred  8085  xpord2indlem  8087  fisn  9330  axdc3lem4  10366  axdc4lem  10368  axcclem  10370  opelreal  11044  seqid3  13999  seqz  14003  1exp  14044  hashf1lem2  14409  fprodn0f  15947  imasaddfnlem  17483  initoid  17959  termoid  17960  0subm  18776  smndex1mgm  18869  smndex1n0mnd  18874  grpinvfval  18945  0subg  19118  0nsg  19135  eqg0subg  19162  kerf1ghm  19213  sylow2alem2  19584  gsumval3  19873  gsumzaddlem  19887  lsssn0  20938  rngqiprngimf1  21293  pzriprnglem8  21463  r0cld  23721  alexsubALTlem2  24031  tgphaus  24100  isusp  24244  i1f1lem  25674  ig1pcl  26162  plyco0  26175  plyeq0lem  26193  plycj  26260  plycjOLD  26262  wilthlem2  27050  dchrfi  27236  mulsval  28119  snstriedgval  29125  incistruhgr  29166  1loopgrnb0  29589  umgr2v2enb1  29613  usgr2pthlem  29849  hsn0elch  31337  h1de2ctlem  31644  atomli  32471  suppiniseg  32778  1stpreimas  32798  gsummpt2d  33130  kerunit  33408  exsslsb  33781  qqhval2lem  34165  qqhf  34170  qqhre  34204  esum2dlem  34276  eulerpartlemb  34552  bnj149  35057  subfacp1lem6  35413  ellimits  36136  weiunse  36696  bj-0nel1  37306  bj-isrvec  37654  poimirlem18  38005  poimirlem21  38008  poimirlem22  38009  poimirlem31  38018  poimirlem32  38019  itg2addnclem2  38039  ftc1anclem3  38062  0idl  38392  keridl  38399  smprngopr  38419  isdmn3  38441  ellkr  39581  diblss  41662  dihmeetlem4preN  41798  dihmeetlem13N  41811  sticksstones11  42641  0prjspnrel  43077  pw2f1ocnv  43482  fvnonrel  44041  snhesn  44230  unirnmapsn  45659  sge0fodjrnlem  46859  isubgr3stgrlem4  48460  usgrexmpl2trifr  48528  lindslinindsimp1  48948