Theorem elsni 3416

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 3413	. 2 |- ( A e. { B } -> ( A e. { B } <-> A = B ) )
2	1	ibi 174	1 |- ( A e. { B } -> A = B )

Syntax hints:   -> wi 4   = wceq 1284   e. wcel 1433   {csn 3398

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 662  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-10 1436  ax-11 1437  ax-i12 1438  ax-bndl 1439  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-nfc 2208  df-v 2603  df-sn 3404

This theorem is referenced by:  elsn2g  3427  disjsn2  3455  sssnm  3546  disjxsn  3783  opth1  3991  elsuci  4158  ordtri2orexmid  4266  onsucsssucexmid  4270  sosng  4431  ressn  4878  funcnvsn  4965  fvconst  5372  fmptap  5374  fmptapd  5375  fvunsng  5378  1stconst  5862  2ndconst  5863  reldmtpos  5891  tpostpos  5902  ac6sfi  6379  onunsnss  6383  snon0  6387  supsnti  6418  elreal2  6999  ax1rid  7043  ltxrlt  7178  un0addcl  8321  un0mulcl  8322  elfzonlteqm1  9219  iseqid3  9465  1exp  9505  divalgmod  10327  bj-nntrans  10746  bj-nnelirr  10748