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

Theorem elsnc 3676
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 3675 . 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 1632    e. wcel 1696   _Vcvv 2801   {csn 3653
This theorem is referenced by:  sneqr  3796  opthwiener  4284  snsn0non  4527  opthprc  4752  dmsnn0  5154  dmsnopg  5160  cnvcnvsn  5166  sniota  5262  funconstss  5659  fniniseg  5662  fniniseg2  5664  fsn  5712  fnse  6248  eusvobj2  6353  fisn  7196  mapfien  7415  axdc3lem4  8095  axdc4lem  8097  axcclem  8099  ttukeylem7  8158  opelreal  8768  seqid3  11106  seqz  11110  1exp  11147  hashf1lem2  11410  imasaddfnlem  13446  0subg  14658  0nsg  14678  sylow2alem2  14945  gsumval3  15207  gsumzaddlem  15219  lsssn0  15721  r0cld  17445  alexsubALTlem2  17758  tgphaus  17815  i1f1lem  19060  ig1pcl  19577  plyco0  19590  plyeq0lem  19608  plycj  19674  wilthlem2  20323  dchrfi  20510  hsn0elch  21843  h1de2ctlem  22150  atomli  22978  subfacp1lem6  23731  wfrlem14  24340  ellimits  24521  itg2addnclem2  25004  itgaddnclem2  25010  0idl  26753  keridl  26760  smprngopr  26780  isdmn3  26802  pw2f1ocnv  27233  bnj149  29223  ellkr  29901  diblss  31982  dihmeetlem4preN  32118  dihmeetlem13N  32131
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sn 3659
  Copyright terms: Public domain W3C validator