Theorem elsni 3593

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

Step	Hyp	Ref	Expression
1		elsng 3590	. 2 |- ( A e. { B } -> ( A e. { B } <-> A = B ) )
2	1	ibi 175	1 |- ( A e. { B } -> A = B )

Syntax hints:   -> wi 4   = wceq 1343   e. wcel 2136   {csn 3575

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 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-bndl 1497  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-nfc 2296  df-v 2727  df-sn 3581

This theorem is referenced by:  elsn2g  3608  nelsn  3610  disjsn2  3638  sssnm  3733  disjxsn  3979  pwntru  4177  opth1  4213  elsuci  4380  ordtri2orexmid  4499  onsucsssucexmid  4503  sosng  4676  ressn  5143  funcnvsn  5232  funinsn  5236  fvconst  5672  fmptap  5674  fmptapd  5675  fvunsng  5678  mposnif  5932  1stconst  6185  2ndconst  6186  reldmtpos  6217  tpostpos  6228  1domsn  6781  ac6sfi  6860  onunsnss  6878  snon0  6897  snexxph  6911  elfi2  6933  supsnti  6966  djuf1olem  7014  eldju2ndl  7033  eldju2ndr  7034  difinfsnlem  7060  pw1on  7178  elreal2  7767  ax1rid  7814  ltxrlt  7960  un0addcl  9143  un0mulcl  9144  elfzonlteqm1  10141  fxnn0nninf  10369  1exp  10480  hashinfuni  10686  hashennnuni  10688  hashprg  10717  zfz1isolemiso  10748  fisumss  11329  sumsnf  11346  fsumsplitsn  11347  fsum2dlemstep  11371  fisumcom2  11375  fprodssdc  11527  fprodunsn  11541  fprod2dlemstep  11559  fprodcom2fi  11563  fprodsplitsn  11570  divalgmod  11860  phi1  12147  dfphi2  12148  nnnn0modprm0  12183  exmidunben  12355  txdis1cn  12878  bj-nntrans  13793  bj-nnelirr  13795  pwtrufal  13837  sssneq  13842  exmidsbthrlem  13861