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

Theorem elsnc 3665
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 3664 . 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 1624    e. wcel 1685   _Vcvv 2790   {csn 3642
This theorem is referenced by:  sneqr  3782  opthwiener  4268  snsn0non  4511  opthprc  4736  dmsnn0  5137  dmsnopg  5143  cnvcnvsn  5149  funconstss  5605  fniniseg  5608  fniniseg2  5610  fsn  5658  fnse  6194  sniota  6280  eusvobj2  6333  fisn  7176  mapfien  7395  axdc3lem4  8075  axdc4lem  8077  axcclem  8079  ttukeylem7  8138  opelreal  8748  seqid3  11085  seqz  11089  1exp  11126  hashf1lem2  11389  imasaddfnlem  13425  0subg  14637  0nsg  14657  sylow2alem2  14924  gsumval3  15186  gsumzaddlem  15198  lsssn0  15700  r0cld  17424  alexsubALTlem2  17737  tgphaus  17794  i1f1lem  19039  ig1pcl  19556  plyco0  19569  plyeq0lem  19587  plycj  19653  wilthlem2  20302  dchrfi  20489  hsn0elch  21820  h1de2ctlem  22127  atomli  22955  subfacp1lem6  23121  wfrlem14  23671  ellimits  23859  0idl  26050  keridl  26057  smprngopr  26077  isdmn3  26099  pw2f1ocnv  26530  bnj149  28175  ellkr  28547  diblss  30628  dihmeetlem4preN  30764  dihmeetlem13N  30777
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-v 2792  df-sn 3648
  Copyright terms: Public domain W3C validator