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

Theorem elsni 3664
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 3662 . 2  |-  ( A  e.  { B }  ->  ( A  e.  { B }  <->  A  =  B
) )
21ibi 232 1  |-  ( A  e.  { B }  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    e. wcel 1684   {csn 3640
This theorem is referenced by:  elsnc2g  3668  disjsn2  3694  sssn  3772  disjxsn  4017  opth1  4244  elsuci  4458  elpwunsn  4568  sosn  4759  ressn  5211  funcnvsn  5297  fvconst  5708  fmptap  5710  fvunsn  5712  1stconst  6207  2ndconst  6208  reldmtpos  6242  tpostpos  6254  disjen  7018  map2xp  7031  ac6sfi  7101  ixpfi2  7154  elfi2  7168  fisn  7180  unxpwdom2  7302  cantnfp1lem3  7382  isfin4-3  7941  dcomex  8073  iundom2g  8162  fpwwe2lem13  8264  canthp1lem2  8275  0tsk  8377  elreal2  8754  ax1rid  8783  ltxrlt  8893  un0addcl  9997  un0mulcl  9998  seqf1o  11087  seqid3  11090  seqz  11094  1exp  11131  hashprg  11368  eqs1  11447  cats1un  11476  fsumss  12198  sumsn  12213  fsum2dlem  12233  fsumcom2  12237  ackbijnn  12286  phi1  12841  dfphi2  12842  ramubcl  13065  0ram  13067  ramz  13072  imasvscafn  13439  xpsc0  13462  xpsc1  13463  xpsfrnel2  13467  mreexmrid  13545  gsumress  14454  gsumval2  14460  0nsg  14662  lsmdisj2  14991  subgdisj1  15000  lt6abl  15181  gsumsn  15220  gsumunsn  15221  gsum2d  15223  dprdfeq0  15257  dprdsn  15271  dprd2da  15277  pgpfac1lem3a  15311  pgpfaclem2  15317  lsssn0  15705  lspsneq0  15769  lspdisjb  15879  lbsextlem4  15914  mplcoe2  16211  coe1tm  16349  frgpcyg  16527  obselocv  16628  obs2ss  16629  obslbs  16630  basdif0  16691  ordtbas  16922  ordtrest2  16934  cmpfi  17135  txdis1cn  17329  ptrescn  17333  txkgen  17346  xkoptsub  17348  ordthmeolem  17492  pt1hmeo  17497  filcon  17578  filufint  17615  flimclslem  17679  ptcmplem3  17748  idnghm  18252  iccpnfcnv  18442  iccpnfhmeo  18443  bndth  18456  ivthicc  18818  ovoliunlem1  18861  i1fima2sn  19035  i1f1  19045  itg1addlem4  19054  itg1addlem5  19055  i1fmulc  19058  limcres  19236  limccnp  19241  limccnp2  19242  degltlem1  19458  ply1rem  19549  fta1blem  19554  ig1pdvds  19562  plyeq0lem  19592  plypf1  19594  plyaddlem1  19595  plymullem1  19596  coemulhi  19635  plycj  19658  taylfval  19738  abelthlem3  19809  rlimcnp  20260  wilthlem2  20307  logexprlim  20464  gidsn  21015  rngosn  21071  rngoueqz  21097  fmptapd  23213  xrge0iifcnv  23315  xrge0iifhom  23319  gsumsn2  23378  xrge0tsmsbi  23383  esumsn  23437  esumpr  23438  measvunilem0  23541  measvuni  23542  derangsn  23701  subfacp1lem5  23715  erdszelem4  23725  erdszelem8  23729  sconpi1  23770  cvmlift2lem6  23839  cvmlift2lem12  23845  vdgr1d  23894  vdgr1b  23895  vdgr1a  23897  eupap1  23900  onint1  24888  fvsnn  25114  basexre  25522  limhun  25570  1ded  25738  1cat  25759  lppotoslem  26143  prdsbnd  26517  rrnequiv  26559  grpokerinj  26575  0rngo  26652  isdmn3  26699  hbtlem5  27332  flcidc  27379  sumsnd  27697  fnchoice  27700  stoweidlem44  27793  wallispi  27819  eldmressn  27982  difprsng  28069  uvtxnbgra  28165  unisnALT  28702  bnj142  28754  bnj98  28899  bnj1442  29079  bnj1452  29082  dibelval2nd  31342  hdmaprnlem9N  32050  hdmap14lem4a  32064
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-sn 3646
  Copyright terms: Public domain W3C validator