Theorem snssd 4571

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 4570	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3792  {csn 4398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-ext 2754

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-v 3400  df-in 3799  df-ss 3806  df-sn 4399

This theorem is referenced by:  sofld  5835  fsnex  6810  fr3nr  7257  wfrlem15  7712  oeeui  7966  ecinxp  8105  ralxpmap  8193  xpdom3  8346  domunsn  8398  mapdom3  8420  isinf  8461  ac6sfi  8492  pwfilem  8548  finsschain  8561  ssfii  8613  marypha1lem  8627  unxpwdom2  8782  en2other2  9165  fseqenlem1  9180  axdc3lem4  9610  axdc4lem  9612  ttukeylem7  9672  fpwwe2lem13  9799  canthwe  9808  canthp1lem1  9809  wuncval2  9904  un0addcl  11677  un0mulcl  11678  ssfzunsnext  12703  fseq1p1m1  12732  hashbclem  13550  hashf1lem1  13553  fsumge1  14933  incexclem  14972  isumltss  14984  fprodsplit1f  15123  rpnnen2lem11  15357  bitsinv1  15570  lcmfunsnlem2  15759  lcmfass  15765  phicl2  15877  vdwlem1  16089  vdwlem8  16096  vdwlem12  16100  vdwlem13  16101  0ram  16128  ramub1lem1  16134  ramub1lem2  16135  ramcl  16137  imasaddfnlem  16574  imasaddflem  16576  imasvscafn  16583  imasvscaf  16585  mrieqvlemd  16675  mreexmrid  16689  mreexexlem4d  16693  acsfiindd  17563  acsmapd  17564  gsumress  17662  gsumvallem2  17758  0subg  18003  cycsubg2cl  18016  pmtrprfv  18256  odf1o1  18371  gex1  18390  sylow2alem1  18416  sylow2alem2  18417  lsm01  18468  lsm02  18469  lsmdisj  18478  lsmdisj2  18479  prmcyg  18681  gsumzadd  18708  gsumconst  18720  gsumdifsnd  18746  gsumpt  18747  gsumxp  18761  dmdprdd  18785  dprdfadd  18806  dprdres  18814  dprdz  18816  dprdsn  18822  dprddisj2  18825  dprd2da  18828  dprd2d2  18830  dmdprdsplit2lem  18831  dpjcntz  18838  dpjdisj  18839  dpjlsm  18840  dpjidcl  18844  ablfacrp  18852  ablfac1eu  18859  pgpfac1lem1  18860  pgpfac1lem3a  18862  pgpfac1lem3  18863  pgpfac1lem5  18865  pgpfaclem2  18868  kerf1ghm  19134  kerf1hrmOLD  19135  lsssn0  19340  lss0ss  19341  lsptpcl  19374  lspsnvsi  19399  lspun0  19406  pwssplit1  19454  lsmpr  19484  lsppr  19488  lspsntri  19492  lspsolvlem  19538  lspsolv  19539  lsppratlem1  19544  lsppratlem3  19546  lsppratlem4  19547  islbs3  19552  lbsextlem4  19558  rsp1  19621  lidlnz  19625  lidldvgen  19652  psrlidm  19800  psrridm  19801  mplmonmul  19861  mulgrhm2  20243  zndvds  20293  mdetdiaglem  20809  mdetrlin  20813  mdetrsca  20814  mdetrsca2  20815  mdetrlin2  20818  mdetunilem5  20827  mdetunilem9  20831  mdetmul  20834  en2top  21197  rest0  21381  ordtrest  21414  iscnp4  21475  cnconst2  21495  cnpdis  21505  ist1-2  21559  cnt1  21562  dishaus  21594  discmp  21610  cmpcld  21614  conncompid  21643  dis2ndc  21672  dislly  21709  dissnref  21740  comppfsc  21744  llycmpkgen2  21762  cmpkgen  21763  1stckgenlem  21765  1stckgen  21766  ptbasfi  21793  txdis  21844  txdis1cn  21847  txcmplem1  21853  xkohaus  21865  xkoptsub  21866  xkoinjcn  21899  snfbas  22078  trnei  22104  isufil2  22120  ufileu  22131  filufint  22132  uffixsn  22137  ufildom1  22138  flimopn  22187  hausflim  22193  flimcf  22194  flimclslem  22196  flimsncls  22198  cnpflf2  22212  cnpflf  22213  fclsneii  22229  fclsfnflim  22239  fcfnei  22247  flfcntr  22255  alexsubALTlem3  22261  alexsubALTlem4  22262  ptcmplem2  22265  cldsubg  22322  snclseqg  22327  qustgphaus  22334  tsmsgsum  22350  tsmsid  22351  tgptsmscld  22362  tsmsxplem1  22364  tsmsxplem2  22365  ust0  22431  ustuqtop1  22453  neipcfilu  22508  prdsdsf  22580  prdsxmetlem  22581  prdsmet  22583  imasdsf1olem  22586  xpsdsval  22594  prdsbl  22704  prdsxmslem2  22742  idnghm  22955  icccmplem2  23034  metnrmlem2  23071  ioombl  23769  volivth  23811  itg11  23895  i1fmulclem  23906  itg2mulclem  23950  itgsplitioo  24041  limcvallem  24072  limcdif  24077  ellimc2  24078  limcflf  24082  limcmpt2  24085  limcres  24087  cnplimc  24088  limccnp  24092  limccnp2  24093  limcco  24094  dvreslem  24110  dvaddbr  24138  dvmulbr  24139  dvcmulf  24145  dvef  24180  dvivth  24210  lhop2  24215  lhop  24216  ply1remlem  24359  fta1blem  24365  ig1peu  24368  ig1pdvds  24373  plyco0  24385  elply2  24389  plyf  24391  elplyr  24394  elplyd  24395  ply1term  24397  ply0  24401  plyeq0lem  24403  plyeq0  24404  plypf1  24405  plyaddlem  24408  plymullem  24409  dgrlem  24422  coef2  24424  coeidlem  24430  plyco  24434  coemulhi  24447  plycj  24470  vieta1  24504  taylf  24552  radcnv0  24607  abelth  24632  rlimcnp  25144  xrlimcnp  25147  amgm  25169  wilthlem2  25247  basellem7  25265  basellem9  25267  ppiprm  25329  chtprm  25331  musumsum  25370  muinv  25371  logexprlim  25402  perfectlem2  25407  dchrhash  25448  rpvmasum2  25653  axlowdimlem7  26297  axlowdimlem10  26300  upgrex  26440  upgr1elem  26460  uvtxnm1nbgr  26752  umgr2v2e  26873  0oo  28216  sh0le  28871  disjiunel  29972  preimane  30035  fnpreimac  30036  fprodeq02  30133  lsatdim  30433  dimkerim  30441  qtopt1  30500  locfinref  30506  ordtrestNEW  30565  esumsnf  30724  esum2dlem  30752  rossros  30841  oms0  30957  carsggect  30978  eulerpartlems  31020  eulerpartlemgc  31022  eulerpartlemgh  31038  eulerpartlemgs2  31040  plymulx0  31224  circlemeth  31320  hgt750lemb  31336  hgt750leme  31338  bnj1452  31719  subfacp1lem1  31760  subfacp1lem5  31765  erdszelem4  31775  erdszelem8  31779  sconnpi1  31820  cvmscld  31854  cvmlift2lem6  31889  cvmlift2lem9  31892  cvmlift2lem11  31894  cvmlift2lem12  31895  mrsubvrs  32018  slerec  32512  neibastop2lem  32943  topjoin  32948  fnejoin2  32952  lindsadd  34028  poimirlem3  34038  poimirlem9  34044  poimirlem28  34063  poimirlem32  34067  prdsbnd  34216  heiborlem8  34241  rrnequiv  34258  grpokerinj  34316  0idl  34448  prnc  34490  isfldidl  34491  lshpnel2N  35139  lsatfixedN  35163  lfl0f  35223  lkrlsp3  35258  elpaddatriN  35957  elpaddat  35958  elpadd2at  35960  pmodlem1  36000  osumcllem1N  36110  osumcllem2N  36111  osumcllem9N  36118  osumcllem10N  36119  pexmidlem6N  36129  pexmidlem7N  36130  dibss  37323  dochocsn  37535  dochsncom  37536  dochnel  37547  dihprrnlem1N  37578  dihprrnlem2  37579  djhlsmat  37581  dihsmsprn  37584  dvh4dimlem  37597  dvhdimlem  37598  dochsnnz  37604  dochsatshp  37605  dochsnshp  37607  dochexmid  37622  dochsnkr  37626  dochsnkr2cl  37628  dochfl1  37630  lcfl7lem  37653  lcfl6  37654  lcfl8  37656  lcfl9a  37659  lclkrlem2a  37661  lclkrlem2c  37663  lclkrlem2d  37664  lclkrlem2e  37665  lclkrlem2j  37670  lclkrlem2o  37675  lclkrlem2p  37676  lclkrlem2s  37679  lclkrlem2v  37682  lcfrlem14  37710  lcfrlem18  37714  lcfrlem19  37715  lcfrlem20  37716  lcfrlem23  37719  lcfrlem25  37721  lcdlkreqN  37776  mapdval4N  37786  mapdsn  37795  mapdhvmap  37923  hdmaprnlem4tN  38006  hdmapinvlem1  38072  hdmapinvlem2  38073  hdmapinvlem3  38074  hdmapinvlem4  38075  hdmapglem5  38076  hgmapvvlem3  38079  hdmapglem7a  38081  hdmapglem7b  38082  hdmapglem7  38083  hdmapoc  38085  elrfi  38217  cmpfiiin  38220  mzpcompact2lem  38274  dfac11  38591  pwssplit4  38618  rngunsnply  38702  flcidc  38703  acsfn1p  38728  proot1mul  38736  iocinico  38755  iunrelexp0  38951  frege81d  38996  k0004lem3  39403  binomcxplemnn0  39504  fsumsplit1  40712  islptre  40759  limciccioolb  40761  limcicciooub  40777  limcresiooub  40782  limcresioolb  40783  ioccncflimc  41026  icccncfext  41028  icocncflimc  41030  cncfiooicc  41035  dvnprodlem2  41090  dirkercncflem2  41248  dirkercncflem3  41249  fourierdlem48  41298  fourierdlem49  41299  fourierdlem79  41329  fourierdlem101  41351  sge0sup  41532  hoidmvlelem2  41737  hoiqssbl  41766  hspmbllem1  41767  hspmbllem2  41768  ovnovollem1  41797  fsumsplitsndif  42375  perfectALTVlem2  42656  1hegrlfgr  42755  gsumdifsndf  43159