Theorem elsni 4029

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

Syntax hints:   -> wi 4   = wceq 1438   e. wcel 1873   {csn 4004

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1664  ax-4 1677  ax-5 1753  ax-6 1799  ax-7 1844  ax-10 1892  ax-11 1897  ax-12 1910  ax-13 2058  ax-ext 2402

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1659  df-nf 1663  df-sb 1792  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-v 3087  df-sn 4005

This theorem is referenced by:  elsnc2g  4034  elpwunsn  4046  eqoreldif  4047  disjsn2  4067  rabsnifsb  4074  sssn  4164  disjxsn  4423  opth1  4700  sosn  4929  ressn  5397  elsuci  5514  funcnvsn  5652  fvconst  6103  fnsnb  6104  fmptap  6108  fvunsn  6117  mpt2snif  6410  1stconst  6901  2ndconst  6902  reldmtpos  6998  tpostpos  7010  disjen  7744  map2xp  7757  ac6sfi  7830  ixpfi2  7887  elfi2  7943  fisn  7956  unxpwdom2  8118  cantnfp1lem3  8199  isfin4-3  8758  dcomex  8890  iundom2g  8978  fpwwe2lem13  9080  canthp1lem2  9091  0tsk  9193  elreal2  9569  ax1rid  9598  ltxrlt  9717  un0addcl  10916  un0mulcl  10917  elfzonlteqm1  12001  seqf1o  12266  seqid3  12269  seqz  12273  1exp  12313  hashnn0pnf  12537  hashprg  12584  cats1un  12840  fsumss  13796  sumsn  13812  fsum2dlem  13836  fsumcom2  13840  ackbijnn  13891  fprodss  14007  fprod2dlem  14039  fprodcom2  14043  fprodsplitsn  14048  lcmfunsnlem2lem1  14616  lcmfunsnlem2lem2  14617  phi1  14726  dfphi2  14727  nnnn0modprm0  14762  ramubcl  14981  0ram  14983  ramz  14988  imasvscafn  15448  xpsc0  15471  xpsc1  15472  xpsfrnel2  15476  mreexmrid  15554  2initoinv  15910  2termoinv  15917  gsumress  16524  gsumval2  16528  0nsg  16867  symgextf1lem  17066  symgextf1  17067  pmtrprfval  17133  psgnsn  17166  lsmdisj2  17337  subgdisj1  17346  lt6abl  17534  gsumsnfd  17589  gsumzunsnd  17593  gsumunsnfd  17594  gsum2dlem2  17608  dprdfeq0  17660  dprdsn  17674  dprd2da  17680  pgpfac1lem3a  17714  pgpfaclem2  17720  lsssn0  18176  lspsneq0  18240  lspdisjb  18354  lbsextlem4  18389  0ring01eq  18500  mplcoe5  18697  coe1tm  18871  frgpcyg  19148  obselocv  19295  obs2ss  19296  obslbs  19297  mat0dim0  19496  mat0dimid  19497  mat0dimscm  19498  mat1dimscm  19504  mavmul0g  19582  mdet0pr  19621  mdetunilem9  19649  cramer0  19719  pmatcollpw3fi1lem1  19814  basdif0  19972  ordtbas  20212  ordtrest2  20224  cmpfi  20427  refun0  20534  txdis1cn  20654  ptrescn  20658  txkgen  20671  xkoptsub  20673  ordthmeolem  20820  pt1hmeo  20825  filcon  20902  filufint  20939  flimclslem  21003  ptcmplem3  21073  idnghm  21768  iccpnfcnv  21976  iccpnfhmeo  21977  bndth  21990  ivthicc  22413  ovoliunlem1  22459  i1fima2sn  22642  i1f1  22652  itg1addlem4  22661  itg1addlem5  22662  i1fmulc  22665  limcres  22845  limccnp  22850  limccnp2  22851  degltlem1  23025  ply1rem  23118  fta1blem  23123  ig1pdvds  23132  ig1pdvdsOLD  23138  plyeq0lem  23168  plypf1  23170  plyaddlem1  23171  plymullem1  23172  coemulhi  23212  plycj  23235  taylfval  23318  abelthlem3  23392  rlimcnp  23895  wilthlem2  23998  logexprlim  24157  tgldim0eq  24551  nbcusgra  25195  uvtxnbgra  25225  clwlkisclwwlklem2a4  25516  vdgr1d  25635  vdgr1b  25636  vdgr1a  25638  eupap1  25708  frgraunss  25727  vdgfrgragt2  25759  frgrancvvdeqlemC  25771  frgrawopreglem2  25777  gidsn  26080  rngosn  26136  rngoueqz  26162  xrge0tsmsbi  28563  submateqlem1  28647  submateqlem2  28648  ordtrest2NEW  28743  xrge0iifcnv  28753  xrge0iifhom  28757  qqhval2  28800  esumsnf  28899  esumpr  28901  esumiun  28929  measvunilem0  29049  measvuni  29050  carsggect  29164  omsmeas  29169  omsmeasOLD  29170  plymulx0  29450  bnj142OLD  29548  bnj98  29692  bnj1442  29872  bnj1452  29875  derangsn  29907  subfacp1lem5  29921  erdszelem4  29931  erdszelem8  29935  sconpi1  29976  cvmlift2lem6  30045  cvmlift2lem12  30051  onint1  31120  bj-1nel0  31521  bj-sngltag  31551  bj-projval  31564  tan2h  31907  ptrest  31909  poimirlem23  31933  poimirlem24  31934  poimirlem25  31935  poimirlem28  31938  poimirlem29  31939  poimirlem30  31940  poimirlem31  31941  poimirlem32  31942  prdsbnd  32095  rrnequiv  32137  grpokerinj  32153  0rngo  32230  isdmn3  32277  dibelval2nd  34695  hdmaprnlem9N  35403  hdmap14lem4a  35417  hbtlem5  35963  flcidc  36016  frege133d  36333  radcnvrat  36639  unisnALT  37302  sumsnd  37326  fnchoice  37329  rnsnf  37425  founiiun0  37432  sumsnf  37595  fsumsplitsn  37596  cncfiooicc  37718  fperdvper  37736  dvnmul  37764  dvmptfprodlem  37765  dvnprodlem1  37767  dvnprodlem2  37768  itgcoscmulx  37792  stoweidlem44  37851  wallispi  37878  fourierdlem49  37965  fourierdlem56  37972  fourierdlem80  37996  fourierdlem93  38009  fourierdlem101  38017  sge00  38132  sge0sn  38135  sge0snmpt  38139  sge0iunmptlemfi  38169  sge0p1  38170  sge0fodjrnlem  38172  sge0snmptf  38193  sge0splitsn  38197  nnfoctbdjlem  38207  meadjiunlem  38217  ismeannd  38219  caratheodorylem1  38261  isomenndlem  38265  hoidmv1le  38326  hoidmvlelem2  38328  hoidmvlelem3  38329  ovnhoilem1  38333  eldmressn  38501  iccpartltu  38615  nnsum3primesprm  38761  bgoldbtbndlem3  38778  nbgr1vtx  39188  c0snmgmhm  39531  zrinitorngc  39619  ldepspr  39885  lmod1zr  39905