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

Theorem elsnc 3637
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 3636 . 2  |-  ( A  e.  _V  ->  ( A  e.  { B } 
<->  A  =  B ) )
31, 2ax-mp 10 1  |-  ( A  e.  { B }  <->  A  =  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    = wceq 1619    e. wcel 1621   _Vcvv 2763   {csn 3614
This theorem is referenced by:  sneqr  3754  opthwiener  4240  snsn0non  4483  opthprc  4724  dmsnn0  5125  dmsnopg  5131  cnvcnvsn  5137  funconstss  5577  fniniseg  5580  fniniseg2  5582  fsn  5630  fnse  6166  sniota  6252  eusvobj2  6305  fisn  7148  mapfien  7367  axdc3lem4  8047  axdc4lem  8049  axcclem  8051  ttukeylem7  8110  opelreal  8720  seqid3  11056  seqz  11060  1exp  11097  hashf1lem2  11359  imasaddfnlem  13392  0subg  14604  0nsg  14624  sylow2alem2  14891  gsumval3  15153  gsumzaddlem  15165  lsssn0  15667  r0cld  17391  alexsubALTlem2  17704  tgphaus  17761  i1f1lem  19006  ig1pcl  19523  plyco0  19536  plyeq0lem  19554  plycj  19620  wilthlem2  20269  dchrfi  20456  hsn0elch  21787  h1de2ctlem  22094  atomli  22922  subfacp1lem6  23088  wfrlem14  23638  ellimits  23826  0idl  26017  keridl  26024  smprngopr  26044  isdmn3  26066  pw2f1ocnv  26497  bnj149  27956  ellkr  28446  diblss  30527  dihmeetlem4preN  30663  dihmeetlem13N  30676
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-sn 3620
  Copyright terms: Public domain W3C validator