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

Theorem snssd 4736
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 4735 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
31, 2syl 17 1 (𝜑 → {𝐴} ⊆ 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wss 3935  {csn 4559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3942  df-ss 3951  df-sn 4560
This theorem is referenced by:  sofld  6038  fsnex  7030  fr3nr  7482  wfrlem15  7960  oeeui  8218  ecinxp  8362  ralxpmap  8449  xpdom3  8604  domunsn  8656  mapdom3  8678  isinf  8720  ac6sfi  8751  pwfilem  8807  finsschain  8820  ssfii  8872  marypha1lem  8886  unxpwdom2  9041  en2other2  9424  fseqenlem1  9439  axdc3lem4  9864  axdc4lem  9866  ttukeylem7  9926  fpwwe2lem13  10053  canthwe  10062  canthp1lem1  10063  wuncval2  10158  un0addcl  11919  un0mulcl  11920  ssfzunsnext  12942  fseq1p1m1  12971  hashbclem  13800  hashf1lem1  13803  fsumge1  15142  incexclem  15181  isumltss  15193  fprodsplit1f  15334  rpnnen2lem11  15567  bitsinv1  15781  lcmfunsnlem2  15974  lcmfass  15980  phicl2  16095  vdwlem1  16307  vdwlem8  16314  vdwlem12  16318  vdwlem13  16319  0ram  16346  ramub1lem1  16352  ramub1lem2  16353  ramcl  16355  imasaddfnlem  16791  imasaddflem  16793  imasvscafn  16800  imasvscaf  16802  mrieqvlemd  16890  mreexmrid  16904  mreexexlem4d  16908  acsfiindd  17777  acsmapd  17778  gsumress  17882  0subm  17972  gsumvallem2  17988  0subg  18244  trivsubgd  18245  trivsubgsnd  18246  trivnsgd  18264  cycsubg2cl  18294  pmtrprfv  18512  odf1o1  18628  gex1  18647  sylow2alem1  18673  sylow2alem2  18674  lsm01  18728  lsm02  18729  lsmdisj  18738  lsmdisj2  18739  prmcyg  18945  gsumzadd  18973  gsumconst  18985  gsumdifsnd  19012  gsumpt  19013  gsumxp  19027  dmdprdd  19052  dprdfadd  19073  dprdres  19081  dprdz  19083  dprdsn  19089  dprddisj2  19092  dprd2da  19095  dprd2d2  19097  dmdprdsplit2lem  19098  dpjcntz  19105  dpjdisj  19106  dpjlsm  19107  dpjidcl  19111  ablfacrp  19119  ablfac1eu  19126  pgpfac1lem1  19127  pgpfac1lem3a  19129  pgpfac1lem3  19130  pgpfac1lem5  19132  pgpfaclem2  19135  kerf1ghm  19428  kerf1hrmOLD  19429  acsfn1p  19509  lsssn0  19650  lss0ss  19651  lsptpcl  19682  lspsnvsi  19707  lspun0  19714  pwssplit1  19762  lsmpr  19792  lsppr  19796  lspsntri  19800  lspsolvlem  19845  lspsolv  19846  lsppratlem1  19850  lsppratlem3  19852  lsppratlem4  19853  islbs3  19858  lbsextlem4  19864  rsp1  19927  lidlnz  19931  lidldvgen  19958  psrlidm  20113  psrridm  20114  mplmonmul  20175  mulgrhm2  20576  zndvds  20626  mdetdiaglem  21137  mdetrlin  21141  mdetrsca  21142  mdetrsca2  21143  mdetrlin2  21146  mdetunilem5  21155  mdetunilem9  21159  mdetmul  21162  en2top  21523  rest0  21707  ordtrest  21740  iscnp4  21801  cnconst2  21821  cnpdis  21831  ist1-2  21885  cnt1  21888  dishaus  21920  discmp  21936  cmpcld  21940  conncompid  21969  dis2ndc  21998  dislly  22035  dissnref  22066  comppfsc  22070  llycmpkgen2  22088  cmpkgen  22089  1stckgenlem  22091  1stckgen  22092  ptbasfi  22119  txdis  22170  txdis1cn  22173  txcmplem1  22179  xkohaus  22191  xkoptsub  22192  xkoinjcn  22225  snfbas  22404  trnei  22430  isufil2  22446  ufileu  22457  filufint  22458  uffixsn  22463  ufildom1  22464  flimopn  22513  hausflim  22519  flimcf  22520  flimclslem  22522  flimsncls  22524  cnpflf2  22538  cnpflf  22539  fclsneii  22555  fclsfnflim  22565  fcfnei  22573  flfcntr  22581  alexsubALTlem3  22587  alexsubALTlem4  22588  ptcmplem2  22591  cldsubg  22648  snclseqg  22653  qustgphaus  22660  tsmsgsum  22676  tsmsid  22677  tgptsmscld  22688  tsmsxplem1  22690  tsmsxplem2  22691  ust0  22757  ustuqtop1  22779  neipcfilu  22834  prdsdsf  22906  prdsxmetlem  22907  prdsmet  22909  imasdsf1olem  22912  xpsdsval  22920  prdsbl  23030  prdsxmslem2  23068  idnghm  23281  icccmplem2  23360  metnrmlem2  23397  ioombl  24095  volivth  24137  itg11  24221  i1fmulclem  24232  itg2mulclem  24276  itgsplitioo  24367  limcvallem  24398  limcdif  24403  ellimc2  24404  limcflf  24408  limcmpt2  24411  limcres  24413  cnplimc  24414  limccnp  24418  limccnp2  24419  limcco  24420  dvreslem  24436  dvaddbr  24464  dvmulbr  24465  dvcmulf  24471  dvef  24506  dvivth  24536  lhop2  24541  lhop  24542  ply1remlem  24685  fta1blem  24691  ig1peu  24694  ig1pdvds  24699  plyco0  24711  elply2  24715  plyf  24717  elplyr  24720  elplyd  24721  ply1term  24723  ply0  24727  plyeq0lem  24729  plyeq0  24730  plypf1  24731  plyaddlem  24734  plymullem  24735  dgrlem  24748  coef2  24750  coeidlem  24756  plyco  24760  coemulhi  24773  plycj  24796  vieta1  24830  taylf  24878  radcnv0  24933  abelth  24958  rlimcnp  25471  xrlimcnp  25474  amgm  25496  wilthlem2  25574  basellem7  25592  basellem9  25594  ppiprm  25656  chtprm  25658  musumsum  25697  muinv  25698  logexprlim  25729  perfectlem2  25734  dchrhash  25775  rpvmasum2  26016  axlowdimlem7  26662  axlowdimlem10  26665  upgrex  26805  upgr1elem  26825  uvtxnm1nbgr  27114  umgr2v2e  27235  0oo  28494  sh0le  29145  disjiunel  30275  preimane  30344  fnpreimac  30345  fprodeq02  30467  s1f1  30547  gsumzresunsn  30619  pmtrcnelor  30663  isprmidlc  30882  qsidomlem2  30884  lsatdim  30915  drngdimgt0  30916  dimkerim  30923  qtopt1  30999  locfinref  31005  ordtrestNEW  31064  esumsnf  31223  esum2dlem  31251  rossros  31339  oms0  31455  carsggect  31476  eulerpartlems  31518  eulerpartlemgc  31520  eulerpartlemgh  31536  eulerpartlemgs2  31538  plymulx0  31717  circlemeth  31811  hgt750lemb  31827  hgt750leme  31829  bnj1452  32222  pthhashvtx  32272  subfacp1lem1  32324  subfacp1lem5  32329  erdszelem4  32339  erdszelem8  32343  sconnpi1  32384  cvmscld  32418  cvmlift2lem6  32453  cvmlift2lem9  32456  cvmlift2lem11  32458  cvmlift2lem12  32459  mrsubvrs  32667  frrlem13  33033  slerec  33175  neibastop2lem  33606  topjoin  33611  fnejoin2  33615  pibt2  34581  lindsadd  34767  poimirlem3  34777  poimirlem9  34783  poimirlem28  34802  poimirlem32  34806  prdsbnd  34954  heiborlem8  34979  rrnequiv  34996  grpokerinj  35054  0idl  35186  prnc  35228  isfldidl  35229  lshpnel2N  36003  lsatfixedN  36027  lfl0f  36087  lkrlsp3  36122  elpaddatriN  36821  elpaddat  36822  elpadd2at  36824  pmodlem1  36864  osumcllem1N  36974  osumcllem2N  36975  osumcllem9N  36982  osumcllem10N  36983  pexmidlem6N  36993  pexmidlem7N  36994  dibss  38187  dochocsn  38399  dochsncom  38400  dochnel  38411  dihprrnlem1N  38442  dihprrnlem2  38443  djhlsmat  38445  dihsmsprn  38448  dvh4dimlem  38461  dvhdimlem  38462  dochsnnz  38468  dochsatshp  38469  dochsnshp  38471  dochexmid  38486  dochsnkr  38490  dochsnkr2cl  38492  dochfl1  38494  lcfl7lem  38517  lcfl6  38518  lcfl8  38520  lcfl9a  38523  lclkrlem2a  38525  lclkrlem2c  38527  lclkrlem2d  38528  lclkrlem2e  38529  lclkrlem2j  38534  lclkrlem2o  38539  lclkrlem2p  38540  lclkrlem2s  38543  lclkrlem2v  38546  lcfrlem14  38574  lcfrlem18  38578  lcfrlem19  38579  lcfrlem20  38580  lcfrlem23  38583  lcfrlem25  38585  lcdlkreqN  38640  mapdval4N  38650  mapdsn  38659  mapdhvmap  38787  hdmaprnlem4tN  38870  hdmapinvlem1  38936  hdmapinvlem2  38937  hdmapinvlem3  38938  hdmapinvlem4  38939  hdmapglem5  38940  hgmapvvlem3  38943  hdmapglem7a  38945  hdmapglem7b  38946  hdmapglem7  38947  hdmapoc  38949  0prjspnrel  39149  elrfi  39171  cmpfiiin  39174  mzpcompact2lem  39228  dfac11  39542  pwssplit4  39569  rngunsnply  39653  flcidc  39654  proot1mul  39679  iocinico  39698  iunrelexp0  39927  frege81d  39972  k0004lem3  40379  mnuunid  40493  binomcxplemnn0  40561  fsumsplit1  41733  islptre  41780  limciccioolb  41782  limcicciooub  41798  limcresiooub  41803  limcresioolb  41804  ioccncflimc  42048  icccncfext  42050  icocncflimc  42052  cncfiooicc  42057  dvnprodlem2  42112  dirkercncflem2  42270  dirkercncflem3  42271  fourierdlem48  42320  fourierdlem49  42321  fourierdlem79  42351  fourierdlem101  42373  sge0sup  42554  hoidmvlelem2  42759  hoiqssbl  42788  hspmbllem1  42789  hspmbllem2  42790  ovnovollem1  42819  fsumsplitsndif  43414  perfectALTVlem2  43734  1hegrlfgr  43854  gsumdifsndf  43935
  Copyright terms: Public domain W3C validator