ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  elsni Unicode version

Theorem elsni 3515
Description: There is only one element in a singleton. (Contributed by NM, 5-Jun-1994.)
Assertion
Ref Expression
elsni  |-  ( A  e.  { B }  ->  A  =  B )

Proof of Theorem elsni
StepHypRef Expression
1 elsng 3512 . 2  |-  ( A  e.  { B }  ->  ( A  e.  { B }  <->  A  =  B
) )
21ibi 175 1  |-  ( A  e.  { B }  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465   {csn 3497
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-sn 3503
This theorem is referenced by:  elsn2g  3528  disjsn2  3556  sssnm  3651  disjxsn  3897  pwntru  4092  opth1  4128  elsuci  4295  ordtri2orexmid  4408  onsucsssucexmid  4412  sosng  4582  ressn  5049  funcnvsn  5138  funinsn  5142  fvconst  5576  fmptap  5578  fmptapd  5579  fvunsng  5582  mposnif  5833  1stconst  6086  2ndconst  6087  reldmtpos  6118  tpostpos  6129  1domsn  6681  ac6sfi  6760  onunsnss  6773  snon0  6792  snexxph  6806  elfi2  6828  supsnti  6860  djuf1olem  6906  eldju2ndl  6925  eldju2ndr  6926  difinfsnlem  6952  elreal2  7606  ax1rid  7653  ltxrlt  7798  un0addcl  8978  un0mulcl  8979  elfzonlteqm1  9955  fxnn0nninf  10179  1exp  10290  hashinfuni  10491  hashennnuni  10493  hashprg  10522  zfz1isolemiso  10550  fisumss  11129  sumsnf  11146  fsumsplitsn  11147  fsum2dlemstep  11171  fisumcom2  11175  divalgmod  11551  phi1  11822  dfphi2  11823  exmidunben  11866  txdis1cn  12374  bj-nntrans  13076  bj-nnelirr  13078  pwtrufal  13119  exmidsbthrlem  13144
  Copyright terms: Public domain W3C validator