Theorem elsni 3550

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

Syntax hints:   -> wi 4   = wceq 1332   e. wcel 1481   {csn 3532

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-v 2691  df-sn 3538

This theorem is referenced by:  elsn2g  3565  disjsn2  3594  sssnm  3689  disjxsn  3935  pwntru  4130  opth1  4166  elsuci  4333  ordtri2orexmid  4446  onsucsssucexmid  4450  sosng  4620  ressn  5087  funcnvsn  5176  funinsn  5180  fvconst  5616  fmptap  5618  fmptapd  5619  fvunsng  5622  mposnif  5873  1stconst  6126  2ndconst  6127  reldmtpos  6158  tpostpos  6169  1domsn  6721  ac6sfi  6800  onunsnss  6813  snon0  6832  snexxph  6846  elfi2  6868  supsnti  6900  djuf1olem  6946  eldju2ndl  6965  eldju2ndr  6966  difinfsnlem  6992  elreal2  7662  ax1rid  7709  ltxrlt  7854  un0addcl  9034  un0mulcl  9035  elfzonlteqm1  10018  fxnn0nninf  10242  1exp  10353  hashinfuni  10555  hashennnuni  10557  hashprg  10586  zfz1isolemiso  10614  fisumss  11193  sumsnf  11210  fsumsplitsn  11211  fsum2dlemstep  11235  fisumcom2  11239  divalgmod  11660  phi1  11931  dfphi2  11932  exmidunben  11975  txdis1cn  12486  bj-nntrans  13320  bj-nnelirr  13322  pwtrufal  13365  sssneq  13370  exmidsbthrlem  13392