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

Theorem elsnc 3567
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 3566 . 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 2727   {csn 3544
This theorem is referenced by:  sneqr  3680  opthwiener  4161  snsn0non  4402  opthprc  4643  dmsnn0  5044  dmsnopg  5050  cnvcnvsn  5056  funconstss  5495  fniniseg  5498  fniniseg2  5500  fsn  5548  fnse  6084  sniota  6170  eusvobj2  6223  fisn  7064  mapfien  7283  axdc3lem4  7963  axdc4lem  7965  axcclem  7967  ttukeylem7  8026  opelreal  8632  seqid3  10968  seqz  10972  1exp  11009  hashf1lem2  11271  imasaddfnlem  13304  0subg  14477  0nsg  14497  sylow2alem2  14764  gsumval3  15026  gsumzaddlem  15038  lsssn0  15540  r0cld  17261  alexsubALTlem2  17574  tgphaus  17631  i1f1lem  18876  ig1pcl  19393  plyco0  19406  plyeq0lem  19424  plycj  19490  wilthlem2  20139  dchrfi  20326  hsn0elch  21657  h1de2ctlem  21964  atomli  22792  subfacp1lem6  22887  wfrlem14  23437  ellimits  23625  0idl  25816  keridl  25823  smprngopr  25843  isdmn3  25865  pw2f1ocnv  26296  bnj149  27596  ellkr  27968  diblss  30049  dihmeetlem4preN  30185  dihmeetlem13N  30198
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-sn 3550
  Copyright terms: Public domain W3C validator