MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsn Structured version   Visualization version   GIF version

Theorem elsn 4543
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
StepHypRef Expression
1 elsn.1 . 2 𝐴 ∈ V
2 elsng 4542 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 209   = wceq 1538  wcel 2112  Vcvv 3444  {csn 4528
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-sn 4529
This theorem is referenced by:  velsn  4544  opthwiener  5372  opthprc  5584  dmsnn0  6035  dmsnopg  6041  cnvcnvsn  6047  snsn0non  6281  funconstss  6807  fniniseg  6811  fniniseg2  6813  fsn  6878  fconstfv  6956  eusvobj2  7132  fnse  7814  wfrlem14  7955  fisn  8879  axdc3lem4  9868  axdc4lem  9870  axcclem  9872  opelreal  10545  seqid3  13414  seqz  13418  1exp  13458  hashf1lem2  13814  fprodn0f  15340  imasaddfnlem  16796  initoid  17260  termoid  17261  0subm  17977  smndex1mgm  18067  smndex1n0mnd  18072  grpinvfval  18137  0subg  18299  0nsg  18316  sylow2alem2  18738  gsumval3  19023  gsumzaddlem  19037  kerf1ghm  19494  lsssn0  19715  r0cld  22346  alexsubALTlem2  22656  tgphaus  22725  isusp  22870  i1f1lem  24296  ig1pcl  24779  plyco0  24792  plyeq0lem  24810  plycj  24877  wilthlem2  25657  dchrfi  25842  snstriedgval  26834  incistruhgr  26875  1loopgrnb0  27295  umgr2v2enb1  27319  usgr2pthlem  27555  hsn0elch  29034  h1de2ctlem  29341  atomli  30168  suppiniseg  30449  brsnop  30456  1stpreimas  30468  gsummpt2d  30737  kerunit  30950  qqhval2lem  31330  qqhf  31335  qqhre  31369  esum2dlem  31459  eulerpartlemb  31734  bnj149  32255  subfacp1lem6  32540  ellimits  33479  bj-0nel1  34384  bj-isrvec  34703  poimirlem18  35068  poimirlem21  35071  poimirlem22  35072  poimirlem31  35081  poimirlem32  35082  itg2addnclem2  35102  ftc1anclem3  35125  0idl  35456  keridl  35463  smprngopr  35483  isdmn3  35505  ellkr  36378  diblss  38459  dihmeetlem4preN  38595  dihmeetlem13N  38608  0prjspnrel  39600  pw2f1ocnv  39965  fvnonrel  40284  snhesn  40474  unirnmapsn  41830  sge0fodjrnlem  43042  lindslinindsimp1  44853
  Copyright terms: Public domain W3C validator