MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsnc Unicode version

Theorem elsnc 3663
Description: There is only one element in a singleton. Exercise 2 of [TakeutiZaring] p. 15. (Contributed by NM, 13-Sep-1995.)
Hypothesis
Ref Expression
elsnc.1  |-  A  e. 
_V
Assertion
Ref Expression
elsnc  |-  ( A  e.  { B }  <->  A  =  B )

Proof of Theorem elsnc
StepHypRef Expression
1 elsnc.1 . 2  |-  A  e. 
_V
2 elsncg 3662 . 2  |-  ( A  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
31, 2ax-mp 8 1  |-  ( A  e.  { B }  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1623    e. wcel 1684   _Vcvv 2788   {csn 3640
This theorem is referenced by:  sneqr  3780  opthwiener  4268  snsn0non  4511  opthprc  4736  dmsnn0  5138  dmsnopg  5144  cnvcnvsn  5150  sniota  5246  funconstss  5643  fniniseg  5646  fniniseg2  5648  fsn  5696  fnse  6232  eusvobj2  6337  fisn  7180  mapfien  7399  axdc3lem4  8079  axdc4lem  8081  axcclem  8083  ttukeylem7  8142  opelreal  8752  seqid3  11090  seqz  11094  1exp  11131  hashf1lem2  11394  imasaddfnlem  13430  0subg  14642  0nsg  14662  sylow2alem2  14929  gsumval3  15191  gsumzaddlem  15203  lsssn0  15705  r0cld  17429  alexsubALTlem2  17742  tgphaus  17799  i1f1lem  19044  ig1pcl  19561  plyco0  19574  plyeq0lem  19592  plycj  19658  wilthlem2  20307  dchrfi  20494  hsn0elch  21827  h1de2ctlem  22134  atomli  22962  subfacp1lem6  23716  wfrlem14  24269  ellimits  24450  0idl  26650  keridl  26657  smprngopr  26677  isdmn3  26699  pw2f1ocnv  27130  bnj149  28907  ellkr  29279  diblss  31360  dihmeetlem4preN  31496  dihmeetlem13N  31509
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
  Copyright terms: Public domain W3C validator