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  5819  fvconst  5827  fmptap  5829  fmptapd  5830  fvunsng  5833  mposnif  6098  1stconst  6367  2ndconst  6368  reldmtpos  6399  tpostpos  6410  1domsn  6976  ac6sfi  7060  onunsnss  7079  snon0  7102  snexxph  7117  elfi2  7139  supsnti  7172  djuf1olem  7220  eldju2ndl  7239  eldju2ndr  7240  difinfsnlem  7266  pw1m  7409  pw1on  7411  elreal2  8017  ax1rid  8064  ltxrlt  8212  un0addcl  9402  un0mulcl  9403  fzodisjsn  10380  elfzonlteqm1  10416  xnn0nnen  10659  fxnn0nninf  10661  seqf1og  10743  1exp  10790  hashinfuni  10999  hashennnuni  11001  hashprg  11030  zfz1isolemiso  11061  cats1un  11253  fisumss  11903  sumsnf  11920  fsumsplitsn  11921  fsum2dlemstep  11945  fisumcom2  11949  fprodssdc  12101  fprodunsn  12115  fprod2dlemstep  12133  fprodcom2fi  12137  fprodsplitsn  12144  divalgmod  12438  phi1  12741  dfphi2  12742  nnnn0modprm0  12778  exmidunben  12997  bassetsnn  13089  gsumress  13428  0nsg  13751  gsumfzsnfd  13882  lsssn0  14334  lspsneq0  14390  txdis1cn  14952  plyaddlem1  15421  plymullem1  15422  plycoeid3  15431  plycj  15435  pw0ss  15883  bj-nntrans  16314  bj-nnelirr  16316  pwtrufal  16363  sssneq  16368  exmidsbthrlem  16390