Theorem elsni 3651

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

Syntax hints:   -> wi 4   = wceq 1373   e. wcel 2176   {csn 3633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-sn 3639

This theorem is referenced by:  elsn2g  3666  nelsn  3668  disjsn2  3696  sssnm  3795  disjxsn  4043  pwntru  4244  opth1  4281  elsuci  4451  ordtri2orexmid  4572  onsucsssucexmid  4576  sosng  4749  elrelimasn  5049  ressn  5224  funcnvsn  5320  funinsn  5324  funopdmsn  5766  fvconst  5774  fmptap  5776  fmptapd  5777  fvunsng  5780  mposnif  6041  1stconst  6309  2ndconst  6310  reldmtpos  6341  tpostpos  6352  1domsn  6916  ac6sfi  6997  onunsnss  7016  snon0  7039  snexxph  7054  elfi2  7076  supsnti  7109  djuf1olem  7157  eldju2ndl  7176  eldju2ndr  7177  difinfsnlem  7203  pw1on  7340  elreal2  7945  ax1rid  7992  ltxrlt  8140  un0addcl  9330  un0mulcl  9331  elfzonlteqm1  10341  xnn0nnen  10584  fxnn0nninf  10586  seqf1og  10668  1exp  10715  hashinfuni  10924  hashennnuni  10926  hashprg  10955  zfz1isolemiso  10986  fisumss  11736  sumsnf  11753  fsumsplitsn  11754  fsum2dlemstep  11778  fisumcom2  11782  fprodssdc  11934  fprodunsn  11948  fprod2dlemstep  11966  fprodcom2fi  11970  fprodsplitsn  11977  divalgmod  12271  phi1  12574  dfphi2  12575  nnnn0modprm0  12611  exmidunben  12830  gsumress  13260  0nsg  13583  gsumfzsnfd  13714  lsssn0  14165  lspsneq0  14221  txdis1cn  14783  plyaddlem1  15252  plymullem1  15253  plycoeid3  15262  plycj  15266  bj-nntrans  15924  bj-nnelirr  15926  pwtrufal  15971  sssneq  15976  exmidsbthrlem  15998