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

Theorem elsni 3677
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 3675 . 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 1632    e. wcel 1696   {csn 3653
This theorem is referenced by:  elsnc2g  3681  disjsn2  3707  sssn  3788  disjxsn  4033  opth1  4260  elsuci  4474  elpwunsn  4584  sosn  4775  ressn  5227  funcnvsn  5313  fvconst  5724  fmptap  5726  fvunsn  5728  1stconst  6223  2ndconst  6224  reldmtpos  6258  tpostpos  6270  disjen  7034  map2xp  7047  ac6sfi  7117  ixpfi2  7170  elfi2  7184  fisn  7196  unxpwdom2  7318  cantnfp1lem3  7398  isfin4-3  7957  dcomex  8089  iundom2g  8178  fpwwe2lem13  8280  canthp1lem2  8291  0tsk  8393  elreal2  8770  ax1rid  8799  ltxrlt  8909  un0addcl  10013  un0mulcl  10014  seqf1o  11103  seqid3  11106  seqz  11110  1exp  11147  hashprg  11384  eqs1  11463  cats1un  11492  fsumss  12214  sumsn  12229  fsum2dlem  12249  fsumcom2  12253  ackbijnn  12302  phi1  12857  dfphi2  12858  ramubcl  13081  0ram  13083  ramz  13088  imasvscafn  13455  xpsc0  13478  xpsc1  13479  xpsfrnel2  13483  mreexmrid  13561  gsumress  14470  gsumval2  14476  0nsg  14678  lsmdisj2  15007  subgdisj1  15016  lt6abl  15197  gsumsn  15236  gsumunsn  15237  gsum2d  15239  dprdfeq0  15273  dprdsn  15287  dprd2da  15293  pgpfac1lem3a  15327  pgpfaclem2  15333  lsssn0  15721  lspsneq0  15785  lspdisjb  15895  lbsextlem4  15930  mplcoe2  16227  coe1tm  16365  frgpcyg  16543  obselocv  16644  obs2ss  16645  obslbs  16646  basdif0  16707  ordtbas  16938  ordtrest2  16950  cmpfi  17151  txdis1cn  17345  ptrescn  17349  txkgen  17362  xkoptsub  17364  ordthmeolem  17508  pt1hmeo  17513  filcon  17594  filufint  17631  flimclslem  17695  ptcmplem3  17764  idnghm  18268  iccpnfcnv  18458  iccpnfhmeo  18459  bndth  18472  ivthicc  18834  ovoliunlem1  18877  i1fima2sn  19051  i1f1  19061  itg1addlem4  19070  itg1addlem5  19071  i1fmulc  19074  limcres  19252  limccnp  19257  limccnp2  19258  degltlem1  19474  ply1rem  19565  fta1blem  19570  ig1pdvds  19578  plyeq0lem  19608  plypf1  19610  plyaddlem1  19611  plymullem1  19612  coemulhi  19651  plycj  19674  taylfval  19754  abelthlem3  19825  rlimcnp  20276  wilthlem2  20323  logexprlim  20480  gidsn  21031  rngosn  21087  rngoueqz  21113  fmptapd  23228  xrge0iifcnv  23330  xrge0iifhom  23334  gsumsn2  23393  xrge0tsmsbi  23398  esumsn  23452  esumpr  23453  measvunilem0  23556  measvuni  23557  derangsn  23716  subfacp1lem5  23730  erdszelem4  23740  erdszelem8  23744  sconpi1  23785  cvmlift2lem6  23854  cvmlift2lem12  23860  vdgr1d  23909  vdgr1b  23910  vdgr1a  23912  eupap1  23915  onint1  24960  fvsnn  25217  basexre  25625  limhun  25673  1ded  25841  1cat  25862  lppotoslem  26246  prdsbnd  26620  rrnequiv  26662  grpokerinj  26678  0rngo  26755  isdmn3  26802  hbtlem5  27435  flcidc  27482  sumsnd  27800  fnchoice  27803  stoweidlem44  27896  wallispi  27922  eldmressn  28087  uvtxnbgra  28306  unisnALT  29018  bnj142  29070  bnj98  29215  bnj1442  29395  bnj1452  29398  dibelval2nd  31964  hdmaprnlem9N  32672  hdmap14lem4a  32686
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-sn 3659
  Copyright terms: Public domain W3C validator