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

Theorem snssd 4715
Description: The singleton of an element of a class is a subset of the class (deduction form). (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 snssi 4714 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wss 3910  {csn 4540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-v 3473  df-in 3917  df-ss 3927  df-sn 4541
This theorem is referenced by:  sofld  6017  fsnex  7013  fr3nr  7469  wfrlem15  7944  oeeui  8203  ecinxp  8347  ralxpmap  8435  xpdom3  8590  domunsn  8643  mapdom3  8665  isinf  8707  ac6sfi  8738  pwfilem  8794  finsschain  8807  ssfii  8859  marypha1lem  8873  unxpwdom2  9028  en2other2  9412  fseqenlem1  9427  axdc3lem4  9852  axdc4lem  9854  ttukeylem7  9914  fpwwe2lem13  10041  canthwe  10050  canthp1lem1  10051  wuncval2  10146  un0addcl  11908  un0mulcl  11909  ssfzunsnext  12935  fseq1p1m1  12964  hashbclem  13794  hashf1lem1  13797  fsumge1  15131  incexclem  15170  isumltss  15182  fprodsplit1f  15323  rpnnen2lem11  15556  bitsinv1  15768  lcmfunsnlem2  15961  lcmfass  15967  phicl2  16082  vdwlem1  16294  vdwlem8  16301  vdwlem12  16305  vdwlem13  16306  0ram  16333  ramub1lem1  16339  ramub1lem2  16340  ramcl  16342  imasaddfnlem  16780  imasaddflem  16782  imasvscafn  16789  imasvscaf  16791  mrieqvlemd  16879  mreexmrid  16893  mreexexlem4d  16897  acsfiindd  17766  acsmapd  17767  gsumress  17871  0subm  17961  gsumvallem2  17977  0subg  18283  trivsubgd  18284  trivsubgsnd  18285  trivnsgd  18303  cycsubg2cl  18333  pmtrprfv  18560  odf1o1  18676  gex1  18695  sylow2alem1  18721  sylow2alem2  18722  lsm01  18776  lsm02  18777  lsmdisj  18786  lsmdisj2  18787  prmcyg  18993  gsumzadd  19021  gsumconst  19033  gsumdifsnd  19060  gsumpt  19061  gsumxp  19075  dmdprdd  19100  dprdfadd  19121  dprdres  19129  dprdz  19131  dprdsn  19137  dprddisj2  19140  dprd2da  19143  dprd2d2  19145  dmdprdsplit2lem  19146  dpjcntz  19153  dpjdisj  19154  dpjlsm  19155  dpjidcl  19159  ablfacrp  19167  ablfac1eu  19174  pgpfac1lem1  19175  pgpfac1lem3a  19177  pgpfac1lem3  19178  pgpfac1lem5  19180  pgpfaclem2  19183  kerf1ghm  19474  acsfn1p  19554  lsssn0  19695  lss0ss  19696  lsptpcl  19727  lspsnvsi  19752  lspun0  19759  pwssplit1  19807  lsmpr  19837  lsppr  19841  lspsntri  19845  lspsolvlem  19890  lspsolv  19891  lsppratlem1  19895  lsppratlem3  19897  lsppratlem4  19898  islbs3  19903  lbsextlem4  19909  rsp1  19973  lidlnz  19977  lidldvgen  20004  psrlidm  20159  psrridm  20160  mplmonmul  20221  mulgrhm2  20622  zndvds  20672  mdetdiaglem  21183  mdetrlin  21187  mdetrsca  21188  mdetrsca2  21189  mdetrlin2  21192  mdetunilem5  21201  mdetunilem9  21205  mdetmul  21208  en2top  21569  rest0  21753  ordtrest  21786  iscnp4  21847  cnconst2  21867  cnpdis  21877  ist1-2  21931  cnt1  21934  dishaus  21966  discmp  21982  cmpcld  21986  conncompid  22015  dis2ndc  22044  dislly  22081  dissnref  22112  comppfsc  22116  llycmpkgen2  22134  cmpkgen  22135  1stckgenlem  22137  1stckgen  22138  ptbasfi  22165  txdis  22216  txdis1cn  22219  txcmplem1  22225  xkohaus  22237  xkoptsub  22238  xkoinjcn  22271  snfbas  22450  trnei  22476  isufil2  22492  ufileu  22503  filufint  22504  uffixsn  22509  ufildom1  22510  flimopn  22559  hausflim  22565  flimcf  22566  flimclslem  22568  flimsncls  22570  cnpflf2  22584  cnpflf  22585  fclsneii  22601  fclsfnflim  22611  fcfnei  22619  flfcntr  22627  alexsubALTlem3  22633  alexsubALTlem4  22634  ptcmplem2  22637  cldsubg  22695  snclseqg  22700  qustgphaus  22707  tsmsgsum  22723  tsmsid  22724  tgptsmscld  22735  tsmsxplem1  22737  tsmsxplem2  22738  ust0  22804  ustuqtop1  22826  neipcfilu  22881  prdsdsf  22953  prdsxmetlem  22954  prdsmet  22956  imasdsf1olem  22959  xpsdsval  22967  prdsbl  23077  prdsxmslem2  23115  idnghm  23328  icccmplem2  23407  metnrmlem2  23444  ioombl  24148  volivth  24190  itg11  24274  i1fmulclem  24285  itg2mulclem  24329  itgsplitioo  24420  limcvallem  24453  limcdif  24458  ellimc2  24459  limcflf  24463  limcmpt2  24466  limcres  24468  cnplimc  24469  limccnp  24473  limccnp2  24474  limcco  24475  dvreslem  24491  dvaddbr  24520  dvmulbr  24521  dvcmulf  24527  dvef  24562  dvivth  24592  lhop2  24597  lhop  24598  ply1remlem  24742  fta1blem  24748  ig1peu  24751  ig1pdvds  24756  plyco0  24768  elply2  24772  plyf  24774  elplyr  24777  elplyd  24778  ply1term  24780  ply0  24784  plyeq0lem  24786  plyeq0  24787  plypf1  24788  plyaddlem  24791  plymullem  24792  dgrlem  24805  coef2  24807  coeidlem  24813  plyco  24817  coemulhi  24830  plycj  24853  vieta1  24887  taylf  24935  radcnv0  24990  abelth  25015  rlimcnp  25530  xrlimcnp  25533  amgm  25555  wilthlem2  25633  basellem7  25651  basellem9  25653  ppiprm  25715  chtprm  25717  musumsum  25756  muinv  25757  logexprlim  25788  perfectlem2  25793  dchrhash  25834  rpvmasum2  26075  axlowdimlem7  26721  axlowdimlem10  26724  upgrex  26864  upgr1elem  26884  uvtxnm1nbgr  27173  umgr2v2e  27294  0oo  28551  sh0le  29202  disjiunel  30333  preimane  30402  fnpreimac  30403  fprodeq02  30526  s1f1  30606  gsumzresunsn  30699  pmtrcnelor  30743  elgrplsmsn  30953  lsmsnorb  30954  isprmidlc  30974  qsidomlem2  30977  mxidlprm  30988  lsatdim  31026  drngdimgt0  31027  dimkerim  31034  qtopt1  31110  locfinref  31116  ordtrestNEW  31172  esumsnf  31331  esum2dlem  31359  rossros  31447  oms0  31563  carsggect  31584  eulerpartlems  31626  eulerpartlemgc  31628  eulerpartlemgh  31644  eulerpartlemgs2  31646  plymulx0  31825  circlemeth  31919  hgt750lemb  31935  hgt750leme  31937  bnj1452  32332  pthhashvtx  32382  subfacp1lem1  32434  subfacp1lem5  32439  erdszelem4  32449  erdszelem8  32453  sconnpi1  32494  cvmscld  32528  cvmlift2lem6  32563  cvmlift2lem9  32566  cvmlift2lem11  32568  cvmlift2lem12  32569  mrsubvrs  32777  frrlem13  33143  slerec  33285  neibastop2lem  33716  topjoin  33721  fnejoin2  33725  pibt2  34718  lindsadd  34932  poimirlem3  34942  poimirlem9  34948  poimirlem28  34967  poimirlem32  34971  prdsbnd  35113  heiborlem8  35138  rrnequiv  35155  grpokerinj  35213  0idl  35345  prnc  35387  isfldidl  35388  lshpnel2N  36163  lsatfixedN  36187  lfl0f  36247  lkrlsp3  36282  elpaddatriN  36981  elpaddat  36982  elpadd2at  36984  pmodlem1  37024  osumcllem1N  37134  osumcllem2N  37135  osumcllem9N  37142  osumcllem10N  37143  pexmidlem6N  37153  pexmidlem7N  37154  dibss  38347  dochocsn  38559  dochsncom  38560  dochnel  38571  dihprrnlem1N  38602  dihprrnlem2  38603  djhlsmat  38605  dihsmsprn  38608  dvh4dimlem  38621  dvhdimlem  38622  dochsnnz  38628  dochsatshp  38629  dochsnshp  38631  dochexmid  38646  dochsnkr  38650  dochsnkr2cl  38652  dochfl1  38654  lcfl7lem  38677  lcfl6  38678  lcfl8  38680  lcfl9a  38683  lclkrlem2a  38685  lclkrlem2c  38687  lclkrlem2d  38688  lclkrlem2e  38689  lclkrlem2j  38694  lclkrlem2o  38699  lclkrlem2p  38700  lclkrlem2s  38703  lclkrlem2v  38706  lcfrlem14  38734  lcfrlem18  38738  lcfrlem19  38739  lcfrlem20  38740  lcfrlem23  38743  lcfrlem25  38745  lcdlkreqN  38800  mapdval4N  38810  mapdsn  38819  mapdhvmap  38947  hdmaprnlem4tN  39030  hdmapinvlem1  39096  hdmapinvlem2  39097  hdmapinvlem3  39098  hdmapinvlem4  39099  hdmapglem5  39100  hgmapvvlem3  39103  hdmapglem7a  39105  hdmapglem7b  39106  hdmapglem7  39107  hdmapoc  39109  0prjspnrel  39420  elrfi  39442  cmpfiiin  39445  mzpcompact2lem  39499  dfac11  39813  pwssplit4  39840  rngunsnply  39924  flcidc  39925  proot1mul  39950  iocinico  39969  iunrelexp0  40210  frege81d  40255  k0004lem3  40662  mnuunid  40796  binomcxplemnn0  40864  fsumsplit1  42033  islptre  42080  limciccioolb  42082  limcicciooub  42098  limcresiooub  42103  limcresioolb  42104  ioccncflimc  42346  icccncfext  42348  icocncflimc  42350  cncfiooicc  42355  dvnprodlem2  42408  dirkercncflem2  42565  dirkercncflem3  42566  fourierdlem48  42615  fourierdlem49  42616  fourierdlem79  42646  fourierdlem101  42668  sge0sup  42849  hoidmvlelem2  43054  hoiqssbl  43083  hspmbllem1  43084  hspmbllem2  43085  ovnovollem1  43114  fsumsplitsndif  43709  imaelsetpreimafv  43731  perfectALTVlem2  44059  1hegrlfgr  44179  gsumdifsndf  44260
  Copyright terms: Public domain W3C validator