Theorem elsni 4005

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

Syntax hints:   -> wi 4   = wceq 1455   e. wcel 1898   {csn 3980

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-sn 3981

This theorem is referenced by:  elsnc2g  4010  elpwunsn  4024  eqoreldif  4025  disjsn2  4045  rabsnifsb  4053  sssn  4143  disjxsn  4410  opth1  4689  sosn  4923  ressn  5391  elsuci  5508  funcnvsn  5646  fvconst  6106  fnsnb  6107  fmptap  6111  fvunsn  6120  mpt2snif  6417  1stconst  6911  2ndconst  6912  reldmtpos  7007  tpostpos  7019  disjen  7755  map2xp  7768  ac6sfi  7841  ixpfi2  7898  elfi2  7954  fisn  7967  unxpwdom2  8129  cantnfp1lem3  8211  isfin4-3  8771  dcomex  8903  iundom2g  8991  fpwwe2lem13  9093  canthp1lem2  9104  0tsk  9206  elreal2  9582  ax1rid  9611  ltxrlt  9730  un0addcl  10932  un0mulcl  10933  elfzonlteqm1  12020  seqf1o  12286  seqid3  12289  seqz  12293  1exp  12333  hashnn0pnf  12557  hashprg  12604  cats1un  12869  fsumss  13840  sumsn  13856  fsum2dlem  13880  fsumcom2  13884  ackbijnn  13935  fprodss  14051  fprod2dlem  14083  fprodcom2  14087  fprodsplitsn  14092  lcmfunsnlem2lem1  14660  lcmfunsnlem2lem2  14661  phi1  14770  dfphi2  14771  nnnn0modprm0  14806  ramubcl  15025  0ram  15027  ramz  15032  imasvscafn  15492  xpsc0  15515  xpsc1  15516  xpsfrnel2  15520  mreexmrid  15598  2initoinv  15954  2termoinv  15961  gsumress  16568  gsumval2  16572  0nsg  16911  symgextf1lem  17110  symgextf1  17111  pmtrprfval  17177  psgnsn  17210  lsmdisj2  17381  subgdisj1  17390  lt6abl  17578  gsumsnfd  17633  gsumzunsnd  17637  gsumunsnfd  17638  gsum2dlem2  17652  dprdfeq0  17704  dprdsn  17718  dprd2da  17724  pgpfac1lem3a  17758  pgpfaclem2  17764  lsssn0  18220  lspsneq0  18284  lspdisjb  18398  lbsextlem4  18433  0ring01eq  18544  mplcoe5  18741  coe1tm  18915  frgpcyg  19193  obselocv  19340  obs2ss  19341  obslbs  19342  mat0dim0  19541  mat0dimid  19542  mat0dimscm  19543  mat1dimscm  19549  mavmul0g  19627  mdet0pr  19666  mdetunilem9  19694  cramer0  19764  pmatcollpw3fi1lem1  19859  basdif0  20017  ordtbas  20257  ordtrest2  20269  cmpfi  20472  refun0  20579  txdis1cn  20699  ptrescn  20703  txkgen  20716  xkoptsub  20718  ordthmeolem  20865  pt1hmeo  20870  filcon  20947  filufint  20984  flimclslem  21048  ptcmplem3  21118  idnghm  21813  iccpnfcnv  22021  iccpnfhmeo  22022  bndth  22035  ivthicc  22458  ovoliunlem1  22504  i1fima2sn  22687  i1f1  22697  itg1addlem4  22706  itg1addlem5  22707  i1fmulc  22710  limcres  22890  limccnp  22895  limccnp2  22896  degltlem1  23070  ply1rem  23163  fta1blem  23168  ig1pdvds  23177  ig1pdvdsOLD  23183  plyeq0lem  23213  plypf1  23215  plyaddlem1  23216  plymullem1  23217  coemulhi  23257  plycj  23280  taylfval  23363  abelthlem3  23437  rlimcnp  23940  wilthlem2  24043  logexprlim  24202  tgldim0eq  24596  nbcusgra  25240  uvtxnbgra  25270  clwlkisclwwlklem2a4  25561  vdgr1d  25680  vdgr1b  25681  vdgr1a  25683  eupap1  25753  frgraunss  25772  vdgfrgragt2  25804  frgrancvvdeqlemC  25816  frgrawopreglem2  25822  gidsn  26125  rngosn  26181  rngoueqz  26207  xrge0tsmsbi  28598  submateqlem1  28682  submateqlem2  28683  ordtrest2NEW  28778  xrge0iifcnv  28788  xrge0iifhom  28792  qqhval2  28835  esumsnf  28934  esumpr  28936  esumiun  28964  measvunilem0  29084  measvuni  29085  carsggect  29199  omsmeas  29204  omsmeasOLD  29205  plymulx0  29485  bnj142OLD  29583  bnj98  29727  bnj1442  29907  bnj1452  29910  derangsn  29942  subfacp1lem5  29956  erdszelem4  29966  erdszelem8  29970  sconpi1  30011  cvmlift2lem6  30080  cvmlift2lem12  30086  onint1  31158  bj-1nel0  31592  bj-sngltag  31622  bj-projval  31635  tan2h  31982  ptrest  31984  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem28  32013  poimirlem29  32014  poimirlem30  32015  poimirlem31  32016  poimirlem32  32017  prdsbnd  32170  rrnequiv  32212  grpokerinj  32228  0rngo  32305  isdmn3  32352  dibelval2nd  34765  hdmaprnlem9N  35473  hdmap14lem4a  35487  hbtlem5  36032  flcidc  36085  frege133d  36402  radcnvrat  36707  unisnALT  37363  sumsnd  37387  fnchoice  37390  rnsnf  37496  founiiun0  37503  sumsnf  37686  fsumsplitsn  37687  cncfiooicc  37810  fperdvper  37828  dvnmul  37856  dvmptfprodlem  37857  dvnprodlem1  37859  dvnprodlem2  37860  itgcoscmulx  37884  stoweidlem44  37943  wallispi  37970  fourierdlem49  38057  fourierdlem56  38064  fourierdlem80  38088  fourierdlem93  38101  fourierdlem101  38109  sge00  38256  sge0sn  38259  sge0snmpt  38263  sge0iunmptlemfi  38293  sge0p1  38294  sge0fodjrnlem  38296  sge0snmptf  38317  sge0splitsn  38321  nnfoctbdjlem  38331  meadjiunlem  38341  ismeannd  38343  caratheodorylem1  38385  isomenndlem  38389  hoidmv1le  38454  hoidmvlelem2  38456  hoidmvlelem3  38457  ovnhoilem1  38461  hoiqssbl  38485  eldmressn  38662  iccpartltu  38777  nnsum3primesprm  38923  bgoldbtbndlem3  38940  elfzr  39109  elfzo0l  39110  elfzlmr  39111  nbgr1vtx  39476  c0snmgmhm  40187  zrinitorngc  40275  ldepspr  40539  lmod1zr  40559