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

Theorem snssd 4175
Description: The singleton of an element of a class is a subset of the class (deduction rule). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypothesis
Ref Expression
snssd.1
Assertion
Ref Expression
snssd

Proof of Theorem snssd
StepHypRef Expression
1 snssd.1 . 2
2 snssg 4163 . . 3
31, 2syl 16 . 2
41, 3mpbid 210 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  e.wcel 1818  C_wss 3475  {csn 4029
This theorem is referenced by:  frirr  4861  sofld  5460  fr3nr  6615  oeeui  7270  ecinxp  7405  ralxpmap  7488  xpdom3  7635  domunsn  7687  mapdom3  7709  isinf  7753  ac6sfi  7784  pwfilem  7834  finsschain  7847  ssfii  7899  marypha1lem  7913  unxpwdom2  8035  mapfienOLD  8159  en2other2  8408  fseqenlem1  8426  axdc3lem4  8854  axdc4lem  8856  ttukeylem7  8916  fpwwe2lem13  9041  canthwe  9050  canthp1lem1  9051  wuncval2  9146  un0addcl  10854  un0mulcl  10855  fseq1p1m1  11781  hashbclem  12501  hashf1lem1  12504  fsumge1  13611  incexclem  13648  isumltss  13660  rpnnen2lem11  13958  bitsinv1  14092  phicl2  14298  vdwlem1  14499  vdwlem8  14506  vdwlem12  14510  vdwlem13  14511  0ram  14538  ramub1lem1  14544  ramub1lem2  14545  ramcl  14547  imasaddfnlem  14925  imasaddflem  14927  imasvscafn  14934  imasvscaf  14936  mrieqvlemd  15026  mreexmrid  15040  mreexexlem4d  15044  acsfiindd  15807  acsmapd  15808  gsumress  15903  gsumvallem2  16003  0subg  16226  cycsubg2cl  16239  pmtrprfv  16478  odf1o1  16592  gex1  16611  sylow2alem1  16637  sylow2alem2  16638  lsm01  16689  lsm02  16690  lsmdisj  16699  lsmdisj2  16700  prmcyg  16896  gsumzadd  16935  gsumzaddOLD  16937  gsumconst  16954  gsumdifsnd  16987  gsumpt  16988  gsumptOLD  16989  gsumxp  17004  gsumxpOLD  17006  dmdprdd  17030  dprdfadd  17060  dprdfaddOLD  17067  dprdres  17075  dprdz  17077  dprdsn  17083  dprddisj2  17087  dprddisj2OLD  17088  dprd2da  17091  dprd2d2  17093  dmdprdsplit2lem  17094  dpjcntz  17101  dpjdisj  17102  dpjlsm  17103  dpjidcl  17107  dpjidclOLD  17114  ablfacrp  17117  ablfac1eu  17124  pgpfac1lem1  17125  pgpfac1lem3a  17127  pgpfac1lem3  17128  pgpfac1lem5  17130  pgpfaclem2  17133  kerf1hrm  17392  lsssn0  17594  lss0ss  17595  lsptpcl  17625  lspsnvsi  17650  lspun0  17657  pwssplit1  17705  lsmpr  17735  lsppr  17739  lspsntri  17743  lspsolvlem  17788  lspsolv  17789  lsppratlem1  17793  lsppratlem3  17795  lsppratlem4  17796  islbs3  17801  lbsextlem4  17807  rsp1  17872  lidlnz  17876  lidldvgen  17903  psrlidm  18056  psrlidmOLD  18057  psrridm  18058  psrridmOLD  18059  mplmonmul  18126  mulgrhm2  18533  mulgrhm2OLD  18536  zndvds  18588  mdetdiaglem  19100  mdetrlin  19104  mdetrsca  19105  mdetrsca2  19106  mdetrlin2  19109  mdetunilem5  19118  mdetunilem9  19122  mdetmul  19125  en2top  19487  rest0  19670  ordtrest  19703  iscnp4  19764  cnconst2  19784  cnpdis  19794  ist1-2  19848  cnt1  19851  dishaus  19883  discmp  19898  cmpcld  19902  concompid  19932  dis2ndc  19961  dislly  19998  dissnref  20029  comppfsc  20033  llycmpkgen2  20051  cmpkgen  20052  1stckgenlem  20054  1stckgen  20055  ptbasfi  20082  txdis  20133  txdis1cn  20136  txcmplem1  20142  xkohaus  20154  xkoptsub  20155  xkoinjcn  20188  pt1hmeo  20307  snfbas  20367  trnei  20393  isufil2  20409  ufileu  20420  filufint  20421  uffixsn  20426  ufildom1  20427  flimopn  20476  hausflim  20482  flimcf  20483  flimclslem  20485  flimsncls  20487  cnpflf2  20501  cnpflf  20502  fclsneii  20518  fclsfnflim  20528  fcfnei  20536  alexsubALTlem3  20549  alexsubALTlem4  20550  ptcmplem2  20553  cldsubg  20609  snclseqg  20614  qustgphaus  20621  tsmsgsum  20637  tsmsid  20638  tsmsgsumOLD  20640  tsmsidOLD  20641  tgptsmscld  20653  tsmsxplem1  20655  tsmsxplem2  20656  ust0  20722  ustuqtop1  20744  neipcfilu  20799  prdsdsf  20870  prdsxmetlem  20871  prdsmet  20873  imasdsf1olem  20876  xpsdsval  20884  prdsbl  20994  prdsxmslem2  21032  idnghm  21250  icccmplem2  21328  metnrmlem2  21364  ioombl  21975  volivth  22016  itg11  22098  i1fmulclem  22109  itg2mulclem  22153  itgsplitioo  22244  limcvallem  22275  limcdif  22280  ellimc2  22281  limcflf  22285  limcmpt2  22288  limcres  22290  cnplimc  22291  limccnp  22295  limccnp2  22296  limcco  22297  dvreslem  22313  dvaddbr  22341  dvmulbr  22342  dvcmulf  22348  dvef  22381  dvivth  22411  lhop2  22416  lhop  22417  ply1remlem  22563  fta1blem  22569  ig1peu  22572  ig1pdvds  22577  plyco0  22589  elply2  22593  plyf  22595  elplyr  22598  elplyd  22599  ply1term  22601  ply0  22605  plyeq0lem  22607  plyeq0  22608  plypf1  22609  plyaddlem  22612  plymullem  22613  dgrlem  22626  coef2  22628  coeidlem  22634  plyco  22638  coemulhi  22651  plycj  22674  vieta1  22708  taylf  22756  radcnv0  22811  abelth  22836  rlimcnp  23295  xrlimcnp  23298  amgm  23320  wilthlem2  23343  basellem7  23360  basellem9  23362  ppiprm  23425  chtprm  23427  musumsum  23468  muinv  23469  logexprlim  23500  perfectlem2  23505  dchrhash  23546  rpvmasum2  23697  axlowdimlem7  24251  axlowdimlem10  24254  umgraex  24323  umgra1  24326  uslgra1  24372  usgra1  24373  uvtxnm1nbgra  24494  constr1trl  24590  eupa0  24974  eupap1  24976  0oo  25704  sh0le  26358  qtopt1  27838  locfinref  27844  ordtrestNEW  27903  esumsn  28072  eulerpartlems  28299  eulerpartlemgc  28301  eulerpartlemgh  28317  eulerpartlemgs2  28319  plymulx0  28504  subfacp1lem1  28623  subfacp1lem5  28628  erdszelem4  28638  erdszelem8  28642  sconpi1  28684  cvmscld  28718  cvmlift2lem6  28753  cvmlift2lem9  28756  cvmlift2lem11  28758  cvmlift2lem12  28759  mrsubvrs  28882  wfrlem15  29357  neibastop2lem  30178  topjoin  30183  fnejoin2  30187  prdsbnd  30289  heiborlem8  30314  rrnequiv  30331  grpokerinj  30347  0idl  30422  prnc  30464  isfldidl  30465  elrfi  30626  cmpfiiin  30629  mzpcompact2lem  30684  dfac11  31008  pwssplit4  31035  rngunsnply  31122  flcidc  31123  acsfn1p  31148  proot1mul  31156  iocinico  31179  binomcxplemnn0  31254  fsumsplit1  31573  islptre  31625  limciccioolb  31627  limcicciooub  31643  limcresiooub  31648  limcresioolb  31649  ioccncflimc  31688  icccncfext  31690  icocncflimc  31692  cncfiooicc  31697  dvnprodlem2  31744  dirkercncflem2  31886  dirkercncflem3  31887  fourierdlem48  31937  fourierdlem49  31938  fourierdlem79  31968  fourierdlem101  31990  fsumsplitsndif  32346  gsumdifsndf  32955  bnj1452  34108  lshpnel2N  34710  lsatfixedN  34734  lfl0f  34794  lkrlsp3  34829  elpaddatriN  35527  elpaddat  35528  elpadd2at  35530  pmodlem1  35570  osumcllem1N  35680  osumcllem2N  35681  osumcllem9N  35688  osumcllem10N  35689  pexmidlem6N  35699  pexmidlem7N  35700  dibss  36896  dochocsn  37108  dochsncom  37109  dochnel  37120  dihprrnlem1N  37151  dihprrnlem2  37152  djhlsmat  37154  dihsmsprn  37157  dvh4dimlem  37170  dvhdimlem  37171  dochsnnz  37177  dochsatshp  37178  dochsnshp  37180  dochexmid  37195  dochsnkr  37199  dochsnkr2cl  37201  dochfl1  37203  lcfl7lem  37226  lcfl6  37227  lcfl8  37229  lcfl9a  37232  lclkrlem2a  37234  lclkrlem2c  37236  lclkrlem2d  37237  lclkrlem2e  37238  lclkrlem2j  37243  lclkrlem2o  37248  lclkrlem2p  37249  lclkrlem2s  37252  lclkrlem2v  37255  lcfrlem14  37283  lcfrlem18  37287  lcfrlem19  37288  lcfrlem20  37289  lcfrlem23  37292  lcfrlem25  37294  lcdlkreqN  37349  mapdval4N  37359  mapdsn  37368  mapdhvmap  37496  hdmaprnlem4tN  37582  hdmapinvlem1  37648  hdmapinvlem2  37649  hdmapinvlem3  37650  hdmapinvlem4  37651  hdmapglem5  37652  hgmapvvlem3  37655  hdmapglem7a  37657  hdmapglem7b  37658  hdmapglem7  37659  hdmapoc  37661
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-v 3111  df-in 3482  df-ss 3489  df-sn 4030
  Copyright terms: Public domain W3C validator