Theorem elsni 3687

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

Syntax hints:   -> wi 4   = wceq 1397   e. wcel 2202   {csn 3669

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-sn 3675

This theorem is referenced by:  elsn2g  3702  nelsn  3704  disjsn2  3732  rabsnifsb  3737  rabsnif  3738  sssnm  3837  disjxsn  4086  pwntru  4289  opth1  4328  elsuci  4500  ordtri2orexmid  4621  onsucsssucexmid  4625  sosng  4799  elrelimasn  5102  ressn  5277  funcnvsn  5375  funinsn  5379  funopdmsn  5834  fvconst  5842  fmptap  5844  fmptapd  5845  fvunsng  5848  mposnif  6115  1stconst  6386  2ndconst  6387  reldmtpos  6419  tpostpos  6430  1domsn  7001  ac6sfi  7087  elssdc  7094  onunsnss  7109  snon0  7134  snexxph  7149  elfi2  7171  supsnti  7204  djuf1olem  7252  eldju2ndl  7271  eldju2ndr  7272  difinfsnlem  7298  pw1m  7442  pw1on  7444  elreal2  8050  ax1rid  8097  ltxrlt  8245  un0addcl  9435  un0mulcl  9436  fzodisjsn  10419  elfzonlteqm1  10456  xnn0nnen  10700  fxnn0nninf  10702  seqf1og  10784  1exp  10831  hashinfuni  11040  hashennnuni  11042  hashprg  11073  zfz1isolemiso  11104  cats1un  11306  fisumss  11971  sumsnf  11988  fsumsplitsn  11989  fsum2dlemstep  12013  fisumcom2  12017  fprodssdc  12169  fprodunsn  12183  fprod2dlemstep  12201  fprodcom2fi  12205  fprodsplitsn  12212  divalgmod  12506  phi1  12809  dfphi2  12810  nnnn0modprm0  12846  exmidunben  13065  bassetsnn  13157  gsumress  13496  0nsg  13819  gsumfzsnfd  13950  lsssn0  14403  lspsneq0  14459  txdis1cn  15021  plyaddlem1  15490  plymullem1  15491  plycoeid3  15500  plycj  15504  pw0ss  15953  usgr1vr  16118  bj-nntrans  16597  bj-nnelirr  16599  pwtrufal  16649  sssneq  16654  exmidsbthrlem  16677  gfsumsn  16737