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

Theorem elsn 4168
 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 4167 . 2 (𝐴 ∈ V → (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵))
31, 2ax-mp 5 1 (𝐴 ∈ {𝐵} ↔ 𝐴 = 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   = wceq 1480   ∈ wcel 1987  Vcvv 3189  {csn 4153 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3191  df-sn 4154 This theorem is referenced by:  velsn  4169  opthwiener  4941  opthprc  5132  dmsnn0  5564  dmsnopg  5570  cnvcnvsn  5576  snsn0non  5810  funconstss  6296  fniniseg  6299  fniniseg2  6301  fsn  6362  fconstfv  6436  eusvobj2  6603  fnse  7246  wfrlem14  7380  fisn  8284  axdc3lem4  9226  axdc4lem  9228  axcclem  9230  opelreal  9902  seqid3  12792  seqz  12796  1exp  12836  hashf1lem2  13185  fprodn0f  14654  imasaddfnlem  16116  initoid  16583  termoid  16584  0subg  17547  0nsg  17567  sylow2alem2  17961  gsumval3  18236  gsumzaddlem  18249  kerf1hrm  18671  lsssn0  18876  r0cld  21460  alexsubALTlem2  21771  tgphaus  21839  isusp  21984  i1f1lem  23375  ig1pcl  23852  plyco0  23865  plyeq0lem  23883  plycj  23950  wilthlem2  24708  dchrfi  24893  snstriedgval  25843  incistruhgr  25883  1loopgrnb0  26297  umgr2v2enb1  26321  usgr2pthlem  26541  hsn0elch  27972  h1de2ctlem  28281  atomli  29108  1stpreimas  29344  gsummpt2d  29584  kerunit  29626  qqhval2lem  29825  qqhf  29830  qqhre  29864  esum2dlem  29953  eulerpartlemb  30229  bnj149  30680  subfacp1lem6  30902  ellimits  31686  bj-0nel1  32614  poimirlem18  33086  poimirlem21  33089  poimirlem22  33090  poimirlem31  33099  poimirlem32  33100  itg2addnclem2  33121  ftc1anclem3  33146  0idl  33483  keridl  33490  smprngopr  33510  isdmn3  33532  ellkr  33883  diblss  35966  dihmeetlem4preN  36102  dihmeetlem13N  36115  pw2f1ocnv  37111  fvnonrel  37411  snhesn  37589  unirnmapsn  38903  sge0fodjrnlem  39961  lindslinindsimp1  41555
 Copyright terms: Public domain W3C validator