MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elsni Structured version   Unicode version

Theorem elsni 3830
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
StepHypRef Expression
1 elsncg 3828 . 2  |-  ( A  e.  { B }  ->  ( A  e.  { B }  <->  A  =  B
) )
21ibi 233 1  |-  ( A  e.  { B }  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    e. wcel 1725   {csn 3806
This theorem is referenced by:  elsnc2g  3834  disjsn2  3861  sssn  3949  disjxsn  4198  opth1  4426  elsuci  4639  elpwunsn  4749  sosn  4939  ressn  5400  funcnvsn  5488  fvconst  5913  fmptap  5915  fvunsn  5917  1stconst  6427  2ndconst  6428  reldmtpos  6479  tpostpos  6491  disjen  7256  map2xp  7269  ac6sfi  7343  ixpfi2  7397  elfi2  7411  fisn  7424  unxpwdom2  7548  cantnfp1lem3  7628  isfin4-3  8187  dcomex  8319  iundom2g  8407  fpwwe2lem13  8509  canthp1lem2  8520  0tsk  8622  elreal2  8999  ax1rid  9028  ltxrlt  9138  un0addcl  10245  un0mulcl  10246  seqf1o  11356  seqid3  11359  seqz  11363  1exp  11401  hashnn0pnf  11618  hashprg  11658  eqs1  11753  cats1un  11782  fsumss  12511  sumsn  12526  fsum2dlem  12546  fsumcom2  12550  ackbijnn  12599  phi1  13154  dfphi2  13155  ramubcl  13378  0ram  13380  ramz  13385  imasvscafn  13754  xpsc0  13777  xpsc1  13778  xpsfrnel2  13782  mreexmrid  13860  gsumress  14769  gsumval2  14775  0nsg  14977  lsmdisj2  15306  subgdisj1  15315  lt6abl  15496  gsumsn  15535  gsumunsn  15536  gsum2d  15538  dprdfeq0  15572  dprdsn  15586  dprd2da  15592  pgpfac1lem3a  15626  pgpfaclem2  15632  lsssn0  16016  lspsneq0  16080  lspdisjb  16190  lbsextlem4  16225  mplcoe2  16522  coe1tm  16657  frgpcyg  16846  obselocv  16947  obs2ss  16948  obslbs  16949  basdif0  17010  ordtbas  17248  ordtrest2  17260  cmpfi  17463  txdis1cn  17659  ptrescn  17663  txkgen  17676  xkoptsub  17678  ordthmeolem  17825  pt1hmeo  17830  filcon  17907  filufint  17944  flimclslem  18008  ptcmplem3  18077  idnghm  18769  iccpnfcnv  18961  iccpnfhmeo  18962  bndth  18975  ivthicc  19347  ovoliunlem1  19390  i1fima2sn  19564  i1f1  19574  itg1addlem4  19583  itg1addlem5  19584  i1fmulc  19587  limcres  19765  limccnp  19770  limccnp2  19771  degltlem1  19987  ply1rem  20078  fta1blem  20083  ig1pdvds  20091  plyeq0lem  20121  plypf1  20123  plyaddlem1  20124  plymullem1  20125  coemulhi  20164  plycj  20187  taylfval  20267  abelthlem3  20341  rlimcnp  20796  wilthlem2  20844  logexprlim  21001  nbcusgra  21464  uvtxnbgra  21494  vdgr1d  21666  vdgr1b  21667  vdgr1a  21669  eupap1  21690  gidsn  21928  rngosn  21984  rngoueqz  22010  fmptapd  24053  gsumsn2  24211  xrge0tsmsbi  24216  xrge0iifcnv  24311  xrge0iifhom  24315  qqhval2  24358  esumsn  24448  esumpr  24449  measvunilem0  24559  measvuni  24560  derangsn  24848  subfacp1lem5  24862  erdszelem4  24872  erdszelem8  24876  sconpi1  24918  cvmlift2lem6  24987  cvmlift2lem12  24993  fprodss  25266  fprod2dlem  25296  fprodcom2  25300  onint1  26191  prdsbnd  26493  rrnequiv  26535  grpokerinj  26551  0rngo  26628  isdmn3  26675  hbtlem5  27300  flcidc  27347  sumsnd  27664  fnchoice  27667  stoweidlem44  27760  wallispi  27786  eldmressn  27951  frgraunss  28322  vdgfrgragt2  28355  frgrancvvdeqlemC  28365  frgrawopreglem2  28371  unisnALT  28975  bnj142  29030  bnj98  29175  bnj1442  29355  bnj1452  29358  dibelval2nd  31887  hdmaprnlem9N  32595  hdmap14lem4a  32609
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-v 2950  df-sn 3812
  Copyright terms: Public domain W3C validator