Theorem elsni 3890

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

Syntax hints:   -> wi 4   = wceq 1362   e. wcel 1755   {csn 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-sn 3866

This theorem is referenced by:  elsnc2g  3895  elpwunsn  3905  disjsn2  3925  rabsnifsb  3931  sssn  4019  disjxsn  4274  opth1  4553  elsuci  4772  sosn  4895  ressn  5361  funcnvsn  5451  fvconst  5884  fnsnb  5885  fmptap  5888  fmptapd  5889  fvunsn  5897  mpt2snif  6173  1stconst  6650  2ndconst  6651  reldmtpos  6742  tpostpos  6754  disjen  7456  map2xp  7469  ac6sfi  7544  ixpfi2  7597  elfi2  7652  fisn  7665  unxpwdom2  7791  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  isfin4-3  8472  dcomex  8604  iundom2g  8692  fpwwe2lem13  8797  canthp1lem2  8808  0tsk  8910  elreal2  9287  ax1rid  9316  ltxrlt  9433  un0addcl  10601  un0mulcl  10602  seqf1o  11831  seqid3  11834  seqz  11838  1exp  11877  hashnn0pnf  12097  hashprg  12139  eqs1  12284  cats1un  12354  fsumss  13186  sumsn  13201  fsum2dlem  13221  fsumcom2  13225  ackbijnn  13274  phi1  13831  dfphi2  13832  nnnn0modprm0  13857  ramubcl  14062  0ram  14064  ramz  14069  imasvscafn  14458  xpsc0  14481  xpsc1  14482  xpsfrnel2  14486  mreexmrid  14564  gsumress  15487  gsumval2  15493  0nsg  15706  symgextf1lem  15905  symgextf1  15906  pmtrprfval  15973  lsmdisj2  16159  subgdisj1  16168  lt6abl  16351  gsumsn  16425  gsumsnd  16426  gsumunsnd  16427  gsum2dlem2  16436  gsum2dOLD  16438  dprdfeq0  16486  dprdfeq0OLD  16493  dprdsn  16507  dprd2da  16515  pgpfac1lem3a  16551  pgpfaclem2  16557  lsssn0  16951  lspsneq0  17015  lspdisjb  17129  lbsextlem4  17164  mplcoe2  17481  mplcoe2OLD  17482  coe1tm  17624  frgpcyg  17848  obselocv  17995  obs2ss  17996  obslbs  17997  mavmul0g  18206  mdet0pr  18245  mdetrsca2  18253  mdetrlin2  18255  mdetunilem5  18264  mdetunilem9  18268  cramer0  18338  basdif0  18400  ordtbas  18638  ordtrest2  18650  cmpfi  18853  txdis1cn  19050  ptrescn  19054  txkgen  19067  xkoptsub  19069  ordthmeolem  19216  pt1hmeo  19221  filcon  19298  filufint  19335  flimclslem  19399  ptcmplem3  19468  idnghm  20164  iccpnfcnv  20358  iccpnfhmeo  20359  bndth  20372  ivthicc  20784  ovoliunlem1  20827  i1fima2sn  21000  i1f1  21010  itg1addlem4  21019  itg1addlem5  21020  i1fmulc  21023  limcres  21203  limccnp  21208  limccnp2  21209  degltlem1  21428  ply1rem  21520  fta1blem  21525  ig1pdvds  21533  plyeq0lem  21563  plypf1  21565  plyaddlem1  21566  plymullem1  21567  coemulhi  21606  plycj  21629  taylfval  21709  abelthlem3  21783  rlimcnp  22244  wilthlem2  22292  logexprlim  22449  tgldim0eq  22838  nbcusgra  23194  uvtxnbgra  23224  vdgr1d  23396  vdgr1b  23397  vdgr1a  23399  eupap1  23420  gidsn  23658  rngosn  23714  rngoueqz  23740  gsumsn2  26092  gsumsnf  26096  gsumunsnf  26097  xrge0tsmsbi  26107  ordtrest2NEW  26207  xrge0iifcnv  26217  xrge0iifhom  26221  qqhval2  26265  esumsn  26369  esumpr  26370  measvunilem0  26481  measvuni  26482  plymulx0  26796  derangsn  26906  subfacp1lem5  26920  erdszelem4  26930  erdszelem8  26934  sconpi1  26976  cvmlift2lem6  27045  cvmlift2lem12  27051  fprodss  27308  fprod2dlem  27338  fprodcom2  27342  onint1  28143  tan2h  28268  ptrest  28269  prdsbnd  28536  rrnequiv  28578  grpokerinj  28594  0rngo  28671  isdmn3  28718  hbtlem5  29329  flcidc  29376  sumsnd  29593  fnchoice  29596  stoweidlem44  29685  wallispi  29711  eldmressn  29873  elfzonlteqm1  30071  clwlkisclwwlklem2a4  30292  frgraunss  30433  vdgfrgragt2  30466  frgrancvvdeqlemC  30478  frgrawopreglem2  30484  psgnsn  30602  0rng01eq  30607  mat0dim0  30643  mat0dimid  30644  mat0dimscm  30645  ldepspr  30716  lmod1zr  30744  unisnALT  31364  bnj142OLD  31419  bnj98  31562  bnj1442  31742  bnj1452  31745  bj-1nel0  32028  bj-sngltag  32059  bj-projval  32072  dibelval2nd  34370  hdmaprnlem9N  35078  hdmap14lem4a  35092