Theorem elsni 3798

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

Syntax hints:   -> wi 4   = wceq 1649   e. wcel 1721   {csn 3774

This theorem is referenced by:  elsnc2g  3802  disjsn2  3829  sssn  3917  disjxsn  4166  opth1  4394  elsuci  4607  elpwunsn  4716  sosn  4906  ressn  5367  funcnvsn  5455  fvconst  5880  fmptap  5882  fvunsn  5884  1stconst  6394  2ndconst  6395  reldmtpos  6446  tpostpos  6458  disjen  7223  map2xp  7236  ac6sfi  7310  ixpfi2  7363  elfi2  7377  fisn  7390  unxpwdom2  7512  cantnfp1lem3  7592  isfin4-3  8151  dcomex  8283  iundom2g  8371  fpwwe2lem13  8473  canthp1lem2  8484  0tsk  8586  elreal2  8963  ax1rid  8992  ltxrlt  9102  un0addcl  10209  un0mulcl  10210  seqf1o  11319  seqid3  11322  seqz  11326  1exp  11364  hashnn0pnf  11581  hashprg  11621  eqs1  11716  cats1un  11745  fsumss  12474  sumsn  12489  fsum2dlem  12509  fsumcom2  12513  ackbijnn  12562  phi1  13117  dfphi2  13118  ramubcl  13341  0ram  13343  ramz  13348  imasvscafn  13717  xpsc0  13740  xpsc1  13741  xpsfrnel2  13745  mreexmrid  13823  gsumress  14732  gsumval2  14738  0nsg  14940  lsmdisj2  15269  subgdisj1  15278  lt6abl  15459  gsumsn  15498  gsumunsn  15499  gsum2d  15501  dprdfeq0  15535  dprdsn  15549  dprd2da  15555  pgpfac1lem3a  15589  pgpfaclem2  15595  lsssn0  15979  lspsneq0  16043  lspdisjb  16153  lbsextlem4  16188  mplcoe2  16485  coe1tm  16620  frgpcyg  16809  obselocv  16910  obs2ss  16911  obslbs  16912  basdif0  16973  ordtbas  17210  ordtrest2  17222  cmpfi  17425  txdis1cn  17620  ptrescn  17624  txkgen  17637  xkoptsub  17639  ordthmeolem  17786  pt1hmeo  17791  filcon  17868  filufint  17905  flimclslem  17969  ptcmplem3  18038  idnghm  18730  iccpnfcnv  18922  iccpnfhmeo  18923  bndth  18936  ivthicc  19308  ovoliunlem1  19351  i1fima2sn  19525  i1f1  19535  itg1addlem4  19544  itg1addlem5  19545  i1fmulc  19548  limcres  19726  limccnp  19731  limccnp2  19732  degltlem1  19948  ply1rem  20039  fta1blem  20044  ig1pdvds  20052  plyeq0lem  20082  plypf1  20084  plyaddlem1  20085  plymullem1  20086  coemulhi  20125  plycj  20148  taylfval  20228  abelthlem3  20302  rlimcnp  20757  wilthlem2  20805  logexprlim  20962  nbcusgra  21425  uvtxnbgra  21455  vdgr1d  21627  vdgr1b  21628  vdgr1a  21630  eupap1  21651  gidsn  21889  rngosn  21945  rngoueqz  21971  fmptapd  24014  gsumsn2  24172  xrge0tsmsbi  24177  xrge0iifcnv  24272  xrge0iifhom  24276  qqhval2  24319  esumsn  24409  esumpr  24410  measvunilem0  24520  measvuni  24521  derangsn  24809  subfacp1lem5  24823  erdszelem4  24833  erdszelem8  24837  sconpi1  24879  cvmlift2lem6  24948  cvmlift2lem12  24954  fprodss  25227  fprod2dlem  25257  fprodcom2  25261  onint1  26103  prdsbnd  26392  rrnequiv  26434  grpokerinj  26450  0rngo  26527  isdmn3  26574  hbtlem5  27200  flcidc  27247  sumsnd  27564  fnchoice  27567  stoweidlem44  27660  wallispi  27686  eldmressn  27851  frgraunss  28099  vdgfrgragt2  28132  frgrancvvdeqlemC  28142  frgrawopreglem2  28148  unisnALT  28747  bnj142  28799  bnj98  28944  bnj1442  29124  bnj1452  29127  dibelval2nd  31635  hdmaprnlem9N  32343  hdmap14lem4a  32357

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-sn 3780