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

Theorem elsn 4605
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 4604 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 205   = wceq 1542  wcel 2107  Vcvv 3447  {csn 4590
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-sn 4591
This theorem is referenced by:  velsn  4606  opthwiener  5475  brsnop  5483  opthprc  5700  dmsnn0  6163  dmsnopg  6169  cnvcnvsn  6175  snsn0non  6446  funconstss  7010  fniniseg  7014  fniniseg2  7016  fsn  7085  fconstfv  7166  eusvobj2  7353  fnse  8069  xpord2pred  8081  xpord2indlem  8083  wfrlem14OLD  8272  fisn  9371  axdc3lem4  10397  axdc4lem  10399  axcclem  10401  opelreal  11074  seqid3  13961  seqz  13965  1exp  14006  hashf1lem2  14364  fprodn0f  15882  imasaddfnlem  17418  initoid  17895  termoid  17896  0subm  18636  smndex1mgm  18725  smndex1n0mnd  18730  grpinvfval  18797  0subg  18961  0subgOLD  18962  0nsg  18979  sylow2alem2  19408  gsumval3  19692  gsumzaddlem  19706  kerf1ghm  20187  lsssn0  20452  r0cld  23112  alexsubALTlem2  23422  tgphaus  23491  isusp  23636  i1f1lem  25076  ig1pcl  25563  plyco0  25576  plyeq0lem  25594  plycj  25661  wilthlem2  26441  dchrfi  26626  mulsval  27403  snstriedgval  28038  incistruhgr  28079  1loopgrnb0  28499  umgr2v2enb1  28523  usgr2pthlem  28760  hsn0elch  30239  h1de2ctlem  30546  atomli  31373  suppiniseg  31654  1stpreimas  31673  gsummpt2d  31947  kerunit  32168  qqhval2lem  32626  qqhf  32631  qqhre  32665  esum2dlem  32755  eulerpartlemb  33032  bnj149  33551  subfacp1lem6  33843  ellimits  34548  bj-0nel1  35474  bj-isrvec  35815  poimirlem18  36146  poimirlem21  36149  poimirlem22  36150  poimirlem31  36159  poimirlem32  36160  itg2addnclem2  36180  ftc1anclem3  36203  0idl  36534  keridl  36541  smprngopr  36561  isdmn3  36583  ellkr  37601  diblss  39683  dihmeetlem4preN  39819  dihmeetlem13N  39832  sticksstones11  40614  0prjspnrel  41012  pw2f1ocnv  41408  fvnonrel  41961  snhesn  42150  unirnmapsn  43526  sge0fodjrnlem  44747  lindslinindsimp1  46628
  Copyright terms: Public domain W3C validator