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

Theorem snssd 4530
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 4529 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2156  wss 3769  {csn 4370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-in 3776  df-ss 3783  df-sn 4371
This theorem is referenced by:  sofld  5792  fsnex  6762  fr3nr  7209  wfrlem15  7665  oeeui  7919  ecinxp  8057  ralxpmap  8144  xpdom3  8297  domunsn  8349  mapdom3  8371  isinf  8412  ac6sfi  8443  pwfilem  8499  finsschain  8512  ssfii  8564  marypha1lem  8578  unxpwdom2  8732  en2other2  9115  fseqenlem1  9130  axdc3lem4  9560  axdc4lem  9562  ttukeylem7  9622  fpwwe2lem13  9749  canthwe  9758  canthp1lem1  9759  wuncval2  9854  un0addcl  11592  un0mulcl  11593  ssfzunsnext  12609  fseq1p1m1  12637  hashbclem  13453  hashf1lem1  13456  fsumge1  14751  incexclem  14790  isumltss  14802  rpnnen2lem11  15173  bitsinv1  15383  lcmfunsnlem2  15572  lcmfass  15578  phicl2  15690  vdwlem1  15902  vdwlem8  15909  vdwlem12  15913  vdwlem13  15914  0ram  15941  ramub1lem1  15947  ramub1lem2  15948  ramcl  15950  imasaddfnlem  16393  imasaddflem  16395  imasvscafn  16402  imasvscaf  16404  mrieqvlemd  16494  mreexmrid  16508  mreexexlem4d  16512  acsfiindd  17382  acsmapd  17383  gsumress  17481  gsumvallem2  17577  0subg  17821  cycsubg2cl  17834  pmtrprfv  18074  odf1o1  18188  gex1  18207  sylow2alem1  18233  sylow2alem2  18234  lsm01  18285  lsm02  18286  lsmdisj  18295  lsmdisj2  18296  prmcyg  18496  gsumzadd  18523  gsumconst  18535  gsumdifsnd  18561  gsumpt  18562  gsumxp  18576  dmdprdd  18600  dprdfadd  18621  dprdres  18629  dprdz  18631  dprdsn  18637  dprddisj2  18640  dprd2da  18643  dprd2d2  18645  dmdprdsplit2lem  18646  dpjcntz  18653  dpjdisj  18654  dpjlsm  18655  dpjidcl  18659  ablfacrp  18667  ablfac1eu  18674  pgpfac1lem1  18675  pgpfac1lem3a  18677  pgpfac1lem3  18678  pgpfac1lem5  18680  pgpfaclem2  18683  kerf1hrm  18947  lsssn0  19152  lss0ss  19153  lsptpcl  19186  lspsnvsi  19211  lspun0  19218  pwssplit1  19266  lsmpr  19296  lsppr  19300  lspsntri  19304  lspsolvlem  19350  lspsolv  19351  lsppratlem1  19356  lsppratlem3  19358  lsppratlem4  19359  islbs3  19364  lbsextlem4  19370  rsp1  19433  lidlnz  19437  lidldvgen  19464  psrlidm  19612  psrridm  19613  mplmonmul  19673  mulgrhm2  20055  zndvds  20105  mdetdiaglem  20615  mdetrlin  20619  mdetrsca  20620  mdetrsca2  20621  mdetrlin2  20624  mdetunilem5  20633  mdetunilem9  20637  mdetmul  20640  en2top  21003  rest0  21187  ordtrest  21220  iscnp4  21281  cnconst2  21301  cnpdis  21311  ist1-2  21365  cnt1  21368  dishaus  21400  discmp  21415  cmpcld  21419  conncompid  21448  dis2ndc  21477  dislly  21514  dissnref  21545  comppfsc  21549  llycmpkgen2  21567  cmpkgen  21568  1stckgenlem  21570  1stckgen  21571  ptbasfi  21598  txdis  21649  txdis1cn  21652  txcmplem1  21658  xkohaus  21670  xkoptsub  21671  xkoinjcn  21704  snfbas  21883  trnei  21909  isufil2  21925  ufileu  21936  filufint  21937  uffixsn  21942  ufildom1  21943  flimopn  21992  hausflim  21998  flimcf  21999  flimclslem  22001  flimsncls  22003  cnpflf2  22017  cnpflf  22018  fclsneii  22034  fclsfnflim  22044  fcfnei  22052  flfcntr  22060  alexsubALTlem3  22066  alexsubALTlem4  22067  ptcmplem2  22070  cldsubg  22127  snclseqg  22132  qustgphaus  22139  tsmsgsum  22155  tsmsid  22156  tgptsmscld  22167  tsmsxplem1  22169  tsmsxplem2  22170  ust0  22236  ustuqtop1  22258  neipcfilu  22313  prdsdsf  22385  prdsxmetlem  22386  prdsmet  22388  imasdsf1olem  22391  xpsdsval  22399  prdsbl  22509  prdsxmslem2  22547  idnghm  22760  icccmplem2  22839  metnrmlem2  22876  ioombl  23546  volivth  23588  itg11  23672  i1fmulclem  23683  itg2mulclem  23727  itgsplitioo  23818  limcvallem  23849  limcdif  23854  ellimc2  23855  limcflf  23859  limcmpt2  23862  limcres  23864  cnplimc  23865  limccnp  23869  limccnp2  23870  limcco  23871  dvreslem  23887  dvaddbr  23915  dvmulbr  23916  dvcmulf  23922  dvef  23957  dvivth  23987  lhop2  23992  lhop  23993  ply1remlem  24136  fta1blem  24142  ig1peu  24145  ig1pdvds  24150  plyco0  24162  elply2  24166  plyf  24168  elplyr  24171  elplyd  24172  ply1term  24174  ply0  24178  plyeq0lem  24180  plyeq0  24181  plypf1  24182  plyaddlem  24185  plymullem  24186  dgrlem  24199  coef2  24201  coeidlem  24207  plyco  24211  coemulhi  24224  plycj  24247  vieta1  24281  taylf  24329  radcnv0  24384  abelth  24409  rlimcnp  24906  xrlimcnp  24909  amgm  24931  wilthlem2  25009  basellem7  25027  basellem9  25029  ppiprm  25091  chtprm  25093  musumsum  25132  muinv  25133  logexprlim  25164  perfectlem2  25169  dchrhash  25210  rpvmasum2  25415  axlowdimlem7  26042  axlowdimlem10  26045  upgrex  26201  upgr1elem  26221  uvtxnm1nbgr  26527  umgr2v2e  26649  0oo  27972  sh0le  28627  disjiunel  29734  fprodeq02  29896  qtopt1  30227  locfinref  30233  ordtrestNEW  30292  esumsnf  30451  esum2dlem  30479  rossros  30568  oms0  30684  carsggect  30705  eulerpartlems  30747  eulerpartlemgc  30749  eulerpartlemgh  30765  eulerpartlemgs2  30767  plymulx0  30949  circlemeth  31043  hgt750lemb  31059  hgt750leme  31061  bnj1452  31443  subfacp1lem1  31484  subfacp1lem5  31489  erdszelem4  31499  erdszelem8  31503  sconnpi1  31544  cvmscld  31578  cvmlift2lem6  31613  cvmlift2lem9  31616  cvmlift2lem11  31618  cvmlift2lem12  31619  mrsubvrs  31742  slerec  32244  neibastop2lem  32676  topjoin  32681  fnejoin2  32685  poimirlem3  33725  poimirlem9  33731  poimirlem28  33750  poimirlem32  33754  prdsbnd  33903  heiborlem8  33928  rrnequiv  33945  grpokerinj  34003  0idl  34135  prnc  34177  isfldidl  34178  lshpnel2N  34765  lsatfixedN  34789  lfl0f  34849  lkrlsp3  34884  elpaddatriN  35583  elpaddat  35584  elpadd2at  35586  pmodlem1  35626  osumcllem1N  35736  osumcllem2N  35737  osumcllem9N  35744  osumcllem10N  35745  pexmidlem6N  35755  pexmidlem7N  35756  dibss  36950  dochocsn  37162  dochsncom  37163  dochnel  37174  dihprrnlem1N  37205  dihprrnlem2  37206  djhlsmat  37208  dihsmsprn  37211  dvh4dimlem  37224  dvhdimlem  37225  dochsnnz  37231  dochsatshp  37232  dochsnshp  37234  dochexmid  37249  dochsnkr  37253  dochsnkr2cl  37255  dochfl1  37257  lcfl7lem  37280  lcfl6  37281  lcfl8  37283  lcfl9a  37286  lclkrlem2a  37288  lclkrlem2c  37290  lclkrlem2d  37291  lclkrlem2e  37292  lclkrlem2j  37297  lclkrlem2o  37302  lclkrlem2p  37303  lclkrlem2s  37306  lclkrlem2v  37309  lcfrlem14  37337  lcfrlem18  37341  lcfrlem19  37342  lcfrlem20  37343  lcfrlem23  37346  lcfrlem25  37348  lcdlkreqN  37403  mapdval4N  37413  mapdsn  37422  mapdhvmap  37550  hdmaprnlem4tN  37633  hdmapinvlem1  37699  hdmapinvlem2  37700  hdmapinvlem3  37701  hdmapinvlem4  37702  hdmapglem5  37703  hgmapvvlem3  37706  hdmapglem7a  37708  hdmapglem7b  37709  hdmapglem7  37710  hdmapoc  37712  elrfi  37759  cmpfiiin  37762  mzpcompact2lem  37816  dfac11  38133  pwssplit4  38160  rngunsnply  38244  flcidc  38245  acsfn1p  38270  proot1mul  38278  iocinico  38297  iunrelexp0  38494  frege81d  38539  k0004lem3  38947  binomcxplemnn0  39048  fsumsplit1  40284  islptre  40331  limciccioolb  40333  limcicciooub  40349  limcresiooub  40354  limcresioolb  40355  ioccncflimc  40578  icccncfext  40580  icocncflimc  40582  cncfiooicc  40587  dvnprodlem2  40642  dirkercncflem2  40800  dirkercncflem3  40801  fourierdlem48  40850  fourierdlem49  40851  fourierdlem79  40881  fourierdlem101  40903  sge0sup  41087  hoidmvlelem2  41292  hoiqssbl  41321  hspmbllem1  41322  hspmbllem2  41323  ovnovollem1  41352  fsumsplitsndif  41918  perfectALTVlem2  42206  1hegrlfgr  42281  gsumdifsndf  42712
  Copyright terms: Public domain W3C validator