Theorem elsni 3684

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

Syntax hints:   -> wi 4   = wceq 1395   e. wcel 2200   {csn 3666

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-sn 3672

This theorem is referenced by:  elsn2g  3699  nelsn  3701  disjsn2  3729  sssnm  3832  disjxsn  4081  pwntru  4283  opth1  4322  elsuci  4494  ordtri2orexmid  4615  onsucsssucexmid  4619  sosng  4792  elrelimasn  5094  ressn  5269  funcnvsn  5366  funinsn  5370  funopdmsn  5823  fvconst  5831  fmptap  5833  fmptapd  5834  fvunsng  5837  mposnif  6104  1stconst  6373  2ndconst  6374  reldmtpos  6405  tpostpos  6416  1domsn  6984  ac6sfi  7068  elssdc  7075  onunsnss  7090  snon0  7113  snexxph  7128  elfi2  7150  supsnti  7183  djuf1olem  7231  eldju2ndl  7250  eldju2ndr  7251  difinfsnlem  7277  pw1m  7420  pw1on  7422  elreal2  8028  ax1rid  8075  ltxrlt  8223  un0addcl  9413  un0mulcl  9414  fzodisjsn  10392  elfzonlteqm1  10428  xnn0nnen  10671  fxnn0nninf  10673  seqf1og  10755  1exp  10802  hashinfuni  11011  hashennnuni  11013  hashprg  11043  zfz1isolemiso  11074  cats1un  11269  fisumss  11919  sumsnf  11936  fsumsplitsn  11937  fsum2dlemstep  11961  fisumcom2  11965  fprodssdc  12117  fprodunsn  12131  fprod2dlemstep  12149  fprodcom2fi  12153  fprodsplitsn  12160  divalgmod  12454  phi1  12757  dfphi2  12758  nnnn0modprm0  12794  exmidunben  13013  bassetsnn  13105  gsumress  13444  0nsg  13767  gsumfzsnfd  13898  lsssn0  14350  lspsneq0  14406  txdis1cn  14968  plyaddlem1  15437  plymullem1  15438  plycoeid3  15447  plycj  15451  pw0ss  15899  bj-nntrans  16397  bj-nnelirr  16399  pwtrufal  16450  sssneq  16455  exmidsbthrlem  16478