Theorem elsn 4542

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

Syntax hints:   ↔ wb 209   = wceq 1543   ∈ wcel 2112  Vcvv 3398  {csn 4527

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-sn 4528

This theorem is referenced by:  velsn  4543  opthwiener  5382  brsnop  5390  opthprc  5598  dmsnn0  6050  dmsnopg  6056  cnvcnvsn  6062  snsn0non  6310  funconstss  6854  fniniseg  6858  fniniseg2  6860  fsn  6928  fconstfv  7006  eusvobj2  7184  fnse  7878  wfrlem14  8046  fisn  9021  axdc3lem4  10032  axdc4lem  10034  axcclem  10036  opelreal  10709  seqid3  13585  seqz  13589  1exp  13629  hashf1lem2  13987  fprodn0f  15516  imasaddfnlem  16987  initoid  17461  termoid  17462  0subm  18198  smndex1mgm  18288  smndex1n0mnd  18293  grpinvfval  18360  0subg  18522  0nsg  18539  sylow2alem2  18961  gsumval3  19246  gsumzaddlem  19260  kerf1ghm  19717  lsssn0  19938  r0cld  22589  alexsubALTlem2  22899  tgphaus  22968  isusp  23113  i1f1lem  24540  ig1pcl  25027  plyco0  25040  plyeq0lem  25058  plycj  25125  wilthlem2  25905  dchrfi  26090  snstriedgval  27083  incistruhgr  27124  1loopgrnb0  27544  umgr2v2enb1  27568  usgr2pthlem  27804  hsn0elch  29283  h1de2ctlem  29590  atomli  30417  suppiniseg  30694  1stpreimas  30712  gsummpt2d  30982  kerunit  31195  qqhval2lem  31597  qqhf  31602  qqhre  31636  esum2dlem  31726  eulerpartlemb  32001  bnj149  32522  subfacp1lem6  32814  xpord2pred  33472  xpord2ind  33474  xpord3pred  33478  ellimits  33898  bj-0nel1  34829  bj-isrvec  35148  poimirlem18  35481  poimirlem21  35484  poimirlem22  35485  poimirlem31  35494  poimirlem32  35495  itg2addnclem2  35515  ftc1anclem3  35538  0idl  35869  keridl  35876  smprngopr  35896  isdmn3  35918  ellkr  36789  diblss  38870  dihmeetlem4preN  39006  dihmeetlem13N  39019  sticksstones11  39781  0prjspnrel  40113  pw2f1ocnv  40503  fvnonrel  40822  snhesn  41012  unirnmapsn  42368  sge0fodjrnlem  43572  lindslinindsimp1  45414