Theorem snssd 4743

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

Step	Hyp	Ref	Expression
1		snssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		snssi 4742	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3888  {csn 4562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905  df-sn 4563

This theorem is referenced by:  sofld  6095  fsnex  7164  fr3nr  7631  frrlem13  8123  wfrlem15OLD  8163  oeeui  8442  ecinxp  8590  ralxpmap  8693  xpdom3  8866  domunsn  8923  mapdom3  8945  pwfilem  8969  isinf  9045  ac6sfi  9067  pwfilemOLD  9122  finsschain  9135  ssfii  9187  marypha1lem  9201  unxpwdom2  9356  en2other2  9774  fseqenlem1  9789  axdc3lem4  10218  axdc4lem  10220  ttukeylem7  10280  fpwwe2lem12  10407  canthwe  10416  canthp1lem1  10417  wuncval2  10512  un0addcl  12275  un0mulcl  12276  ssfzunsnext  13310  fseq1p1m1  13339  hashbclem  14173  hashf1lem1  14177  hashf1lem1OLD  14178  fsumsplit1  15466  fsumge1  15518  incexclem  15557  isumltss  15569  fprodsplit1f  15709  rpnnen2lem11  15942  bitsinv1  16158  lcmfunsnlem2  16354  lcmfass  16360  phicl2  16478  vdwlem1  16691  vdwlem8  16698  vdwlem12  16702  vdwlem13  16703  0ram  16730  ramub1lem1  16736  ramub1lem2  16737  ramcl  16739  imasaddfnlem  17248  imasaddflem  17250  imasvscafn  17257  imasvscaf  17259  mrieqvlemd  17347  mreexmrid  17361  mreexexlem4d  17365  acsfiindd  18280  acsmapd  18281  gsumress  18375  0subm  18465  gsumvallem2  18481  0subg  18789  trivsubgd  18790  trivsubgsnd  18791  trivnsgd  18809  cycsubg2cl  18839  pmtrprfv  19070  odf1o1  19186  gex1  19205  sylow2alem1  19231  sylow2alem2  19232  lsm01  19286  lsm02  19287  lsmdisj  19296  lsmdisj2  19297  prmcyg  19504  gsumzadd  19532  gsumconst  19544  gsumdifsnd  19571  gsumpt  19572  gsumxp  19586  dmdprdd  19611  dprdfadd  19632  dprdres  19640  dprdz  19642  dprdsn  19648  dprddisj2  19651  dprd2da  19654  dprd2d2  19656  dmdprdsplit2lem  19657  dpjcntz  19664  dpjdisj  19665  dpjlsm  19666  dpjidcl  19670  ablfacrp  19678  ablfac1eu  19685  pgpfac1lem1  19686  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfac1lem5  19691  pgpfaclem2  19694  kerf1ghm  19996  acsfn1p  20076  lsssn0  20218  lss0ss  20219  lsptpcl  20250  lspsnvsi  20275  lspun0  20282  pwssplit1  20330  lsmpr  20360  lsppr  20364  lspsntri  20368  lspsolvlem  20413  lspsolv  20414  lsppratlem1  20418  lsppratlem3  20420  lsppratlem4  20421  islbs3  20426  lbsextlem4  20432  rsp1  20504  lidlnz  20508  lidldvgen  20535  mulgrhm2  20709  zndvds  20766  psrlidm  21181  psrridm  21182  mplmonmul  21246  mdetdiaglem  21756  mdetrlin  21760  mdetrsca  21761  mdetrsca2  21762  mdetrlin2  21765  mdetunilem5  21774  mdetunilem9  21778  mdetmul  21781  en2top  22144  rest0  22329  ordtrest  22362  iscnp4  22423  cnconst2  22443  cnpdis  22453  ist1-2  22507  cnt1  22510  dishaus  22542  discmp  22558  cmpcld  22562  conncompid  22591  dis2ndc  22620  dislly  22657  dissnref  22688  comppfsc  22692  llycmpkgen2  22710  cmpkgen  22711  1stckgenlem  22713  1stckgen  22714  ptbasfi  22741  txdis  22792  txdis1cn  22795  txcmplem1  22801  xkohaus  22813  xkoptsub  22814  xkoinjcn  22847  snfbas  23026  trnei  23052  isufil2  23068  ufileu  23079  filufint  23080  uffixsn  23085  ufildom1  23086  flimopn  23135  hausflim  23141  flimcf  23142  flimclslem  23144  flimsncls  23146  cnpflf2  23160  cnpflf  23161  fclsneii  23177  fclsfnflim  23187  fcfnei  23195  flfcntr  23203  alexsubALTlem3  23209  alexsubALTlem4  23210  ptcmplem2  23213  cldsubg  23271  snclseqg  23276  qustgphaus  23283  tsmsgsum  23299  tsmsid  23300  tgptsmscld  23311  tsmsxplem1  23313  tsmsxplem2  23314  ust0  23380  ustuqtop1  23402  neipcfilu  23457  prdsdsf  23529  prdsxmetlem  23530  prdsmet  23532  imasdsf1olem  23535  xpsdsval  23543  prdsbl  23656  prdsxmslem2  23694  idnghm  23916  icccmplem2  23995  metnrmlem2  24032  ioombl  24738  volivth  24780  itg11  24864  i1fmulclem  24876  itg2mulclem  24920  itgsplitioo  25011  limcvallem  25044  limcdif  25049  ellimc2  25050  limcflf  25054  limcmpt2  25057  limcres  25059  cnplimc  25060  limccnp  25064  limccnp2  25065  limcco  25066  dvreslem  25082  dvaddbr  25111  dvmulbr  25112  dvcmulf  25118  dvef  25153  dvivth  25183  lhop2  25188  lhop  25189  ply1remlem  25336  fta1blem  25342  ig1peu  25345  ig1pdvds  25350  plyco0  25362  elply2  25366  plyf  25368  elplyr  25371  elplyd  25372  ply1term  25374  ply0  25378  plyeq0lem  25380  plyeq0  25381  plypf1  25382  plyaddlem  25385  plymullem  25386  dgrlem  25399  coef2  25401  coeidlem  25407  plyco  25411  coemulhi  25424  plycj  25447  vieta1  25481  taylf  25529  radcnv0  25584  abelth  25609  rlimcnp  26124  xrlimcnp  26127  amgm  26149  wilthlem2  26227  basellem7  26245  basellem9  26247  ppiprm  26309  chtprm  26311  musumsum  26350  muinv  26351  logexprlim  26382  perfectlem2  26387  dchrhash  26428  rpvmasum2  26669  axlowdimlem7  27325  axlowdimlem10  27328  upgrex  27471  upgr1elem  27491  uvtxnm1nbgr  27780  umgr2v2e  27901  0oo  29160  sh0le  29811  disjiunel  30944  preimane  31016  fnpreimac  31017  fsuppinisegfi  31030  fprodeq02  31146  s1f1  31226  gsumzresunsn  31323  gsumhashmul  31325  pmtrcnelor  31369  elgrplsmsn  31587  lsmsnorb  31588  grplsm0l  31600  grplsmid  31601  0ringidl  31614  isprmidlc  31632  qsidomlem2  31638  mxidlprm  31649  lsatdim  31709  drngdimgt0  31710  dimkerim  31717  qtopt1  31794  locfinref  31800  zarcls0  31827  zarmxt1  31839  zarcmplem  31840  ordtrestNEW  31880  esumsnf  32041  esum2dlem  32069  rossros  32157  oms0  32273  carsggect  32294  eulerpartlems  32336  eulerpartlemgc  32338  eulerpartlemgh  32354  eulerpartlemgs2  32356  plymulx0  32535  circlemeth  32629  hgt750lemb  32645  hgt750leme  32647  bnj1452  33041  pthhashvtx  33098  subfacp1lem1  33150  subfacp1lem5  33155  erdszelem4  33165  erdszelem8  33169  sconnpi1  33210  cvmscld  33244  cvmlift2lem6  33279  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift2lem12  33285  mrsubvrs  33493  slerec  34022  cofcutr  34101  neibastop2lem  34558  topjoin  34563  fnejoin2  34567  pibt2  35597  lindsadd  35779  poimirlem3  35789  poimirlem9  35795  poimirlem28  35814  poimirlem32  35818  prdsbnd  35960  heiborlem8  35985  rrnequiv  36002  grpokerinj  36060  0idl  36192  prnc  36234  isfldidl  36235  lshpnel2N  37006  lsatfixedN  37030  lfl0f  37090  lkrlsp3  37125  elpaddatriN  37824  elpaddat  37825  elpadd2at  37827  pmodlem1  37867  osumcllem1N  37977  osumcllem2N  37978  osumcllem9N  37985  osumcllem10N  37986  pexmidlem6N  37996  pexmidlem7N  37997  dibss  39190  dochocsn  39402  dochsncom  39403  dochnel  39414  dihprrnlem1N  39445  dihprrnlem2  39446  djhlsmat  39448  dihsmsprn  39451  dvh4dimlem  39464  dvhdimlem  39465  dochsnnz  39471  dochsatshp  39472  dochsnshp  39474  dochexmid  39489  dochsnkr  39493  dochsnkr2cl  39495  dochfl1  39497  lcfl7lem  39520  lcfl6  39521  lcfl8  39523  lcfl9a  39526  lclkrlem2a  39528  lclkrlem2c  39530  lclkrlem2d  39531  lclkrlem2e  39532  lclkrlem2j  39537  lclkrlem2o  39542  lclkrlem2p  39543  lclkrlem2s  39546  lclkrlem2v  39549  lcfrlem14  39577  lcfrlem18  39581  lcfrlem19  39582  lcfrlem20  39583  lcfrlem23  39586  lcfrlem25  39588  lcdlkreqN  39643  mapdval4N  39653  mapdsn  39662  mapdhvmap  39790  hdmaprnlem4tN  39873  hdmapinvlem1  39939  hdmapinvlem2  39940  hdmapinvlem3  39941  hdmapinvlem4  39942  hdmapglem5  39943  hgmapvvlem3  39946  hdmapglem7a  39948  hdmapglem7b  39949  hdmapglem7  39950  hdmapoc  39952  sticksstones9  40117  sticksstones11  40119  evlsbagval  40282  0prjspnrel  40471  elrfi  40523  cmpfiiin  40526  mzpcompact2lem  40580  dfac11  40894  pwssplit4  40921  rngunsnply  41005  flcidc  41006  proot1mul  41031  iocinico  41050  iunrelexp0  41317  frege81d  41362  k0004lem3  41766  mnuunid  41902  binomcxplemnn0  41974  islptre  43167  limciccioolb  43169  limcicciooub  43185  limcresiooub  43190  limcresioolb  43191  ioccncflimc  43433  icccncfext  43435  icocncflimc  43437  cncfiooicc  43442  dvnprodlem2  43495  dirkercncflem2  43652  dirkercncflem3  43653  fourierdlem48  43702  fourierdlem49  43703  fourierdlem79  43733  fourierdlem101  43755  sge0sup  43936  hoidmvlelem2  44141  hoiqssbl  44170  hspmbllem1  44171  hspmbllem2  44172  ovnovollem1  44201  fsumsplitsndif  44836  imaelsetpreimafv  44858  perfectALTVlem2  45185  1hegrlfgr  45305  gsumdifsndf  45386  sepfsepc  46232