Theorem snssd 4812

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3948  {csn 4628

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 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3955  df-ss 3965  df-sn 4629

This theorem is referenced by:  intidg  5457  sofld  6184  fsnex  7278  fr3nr  7756  frrlem13  8280  wfrlem15OLD  8320  oeeui  8599  naddunif  8689  naddasslem1  8690  naddasslem2  8691  ecinxp  8783  ralxpmap  8887  xpdom3  9067  domunsn  9124  mapdom3  9146  pwfilem  9174  isinf  9257  isinfOLD  9258  ac6sfi  9284  pwfilemOLD  9343  finsschain  9356  ssfii  9411  marypha1lem  9425  unxpwdom2  9580  en2other2  10001  fseqenlem1  10016  axdc3lem4  10445  axdc4lem  10447  ttukeylem7  10507  fpwwe2lem12  10634  canthwe  10643  canthp1lem1  10644  wuncval2  10739  un0addcl  12502  un0mulcl  12503  ssfzunsnext  13543  fseq1p1m1  13572  hashbclem  14408  hashf1lem1  14412  hashf1lem1OLD  14413  fsumsplit1  15688  fsumge1  15740  incexclem  15779  isumltss  15791  fprodsplit1f  15931  rpnnen2lem11  16164  bitsinv1  16380  lcmfunsnlem2  16574  lcmfass  16580  phicl2  16698  vdwlem1  16911  vdwlem8  16918  vdwlem12  16922  vdwlem13  16923  0ram  16950  ramub1lem1  16956  ramub1lem2  16957  ramcl  16959  imasaddfnlem  17471  imasaddflem  17473  imasvscafn  17480  imasvscaf  17482  mrieqvlemd  17570  mreexmrid  17584  mreexexlem4d  17588  acsfiindd  18503  acsmapd  18504  gsumress  18598  0subm  18695  gsumvallem2  18712  0subgOLD  19027  trivsubgd  19028  trivsubgsnd  19029  trivnsgd  19047  cycsubg2cl  19083  pmtrprfv  19316  odf1o1  19435  gex1  19454  sylow2alem1  19480  sylow2alem2  19481  lsm01  19534  lsm02  19535  lsmdisj  19544  lsmdisj2  19545  prmcyg  19757  gsumzadd  19785  gsumconst  19797  gsumdifsnd  19824  gsumpt  19825  gsumxp  19839  dmdprdd  19864  dprdfadd  19885  dprdres  19893  dprdz  19895  dprdsn  19901  dprddisj2  19904  dprd2da  19907  dprd2d2  19909  dmdprdsplit2lem  19910  dpjcntz  19917  dpjdisj  19918  dpjlsm  19919  dpjidcl  19923  ablfacrp  19931  ablfac1eu  19938  pgpfac1lem1  19939  pgpfac1lem3a  19941  pgpfac1lem3  19942  pgpfac1lem5  19944  pgpfaclem2  19947  kerf1ghm  20275  acsfn1p  20408  lsssn0  20551  lss0ss  20552  lsptpcl  20583  lspsnvsi  20608  lspun0  20615  pwssplit1  20663  lsmpr  20693  lsppr  20697  lspsntri  20701  lspsolvlem  20748  lspsolv  20749  lsppratlem1  20753  lsppratlem3  20755  lsppratlem4  20756  islbs3  20761  lbsextlem4  20767  rsp1  20842  lidlnz  20846  lidldvgen  20886  mulgrhm2  21040  zndvds  21097  psrlidm  21515  psrridm  21516  mplmonmul  21583  mdetdiaglem  22092  mdetrlin  22096  mdetrsca  22097  mdetrsca2  22098  mdetrlin2  22101  mdetunilem5  22110  mdetunilem9  22114  mdetmul  22117  en2top  22480  rest0  22665  ordtrest  22698  iscnp4  22759  cnconst2  22779  cnpdis  22789  ist1-2  22843  cnt1  22846  dishaus  22878  discmp  22894  cmpcld  22898  conncompid  22927  dis2ndc  22956  dislly  22993  dissnref  23024  comppfsc  23028  llycmpkgen2  23046  cmpkgen  23047  1stckgenlem  23049  1stckgen  23050  ptbasfi  23077  txdis  23128  txdis1cn  23131  txcmplem1  23137  xkohaus  23149  xkoptsub  23150  xkoinjcn  23183  snfbas  23362  trnei  23388  isufil2  23404  ufileu  23415  filufint  23416  uffixsn  23421  ufildom1  23422  flimopn  23471  hausflim  23477  flimcf  23478  flimclslem  23480  flimsncls  23482  cnpflf2  23496  cnpflf  23497  fclsneii  23513  fclsfnflim  23523  fcfnei  23531  flfcntr  23539  alexsubALTlem3  23545  alexsubALTlem4  23546  ptcmplem2  23549  cldsubg  23607  snclseqg  23612  qustgphaus  23619  tsmsgsum  23635  tsmsid  23636  tgptsmscld  23647  tsmsxplem1  23649  tsmsxplem2  23650  ust0  23716  ustuqtop1  23738  neipcfilu  23793  prdsdsf  23865  prdsxmetlem  23866  prdsmet  23868  imasdsf1olem  23871  xpsdsval  23879  prdsbl  23992  prdsxmslem2  24030  idnghm  24252  icccmplem2  24331  metnrmlem2  24368  ioombl  25074  volivth  25116  itg11  25200  i1fmulclem  25212  itg2mulclem  25256  itgsplitioo  25347  limcvallem  25380  limcdif  25385  ellimc2  25386  limcflf  25390  limcmpt2  25393  limcres  25395  cnplimc  25396  limccnp  25400  limccnp2  25401  limcco  25402  dvreslem  25418  dvaddbr  25447  dvmulbr  25448  dvcmulf  25454  dvef  25489  dvivth  25519  lhop2  25524  lhop  25525  ply1remlem  25672  fta1blem  25678  ig1peu  25681  ig1pdvds  25686  plyco0  25698  elply2  25702  plyf  25704  elplyr  25707  elplyd  25708  ply1term  25710  ply0  25714  plyeq0lem  25716  plyeq0  25717  plypf1  25718  plyaddlem  25721  plymullem  25722  dgrlem  25735  coef2  25737  coeidlem  25743  plyco  25747  coemulhi  25760  plycj  25783  vieta1  25817  taylf  25865  radcnv0  25920  abelth  25945  rlimcnp  26460  xrlimcnp  26463  amgm  26485  wilthlem2  26563  basellem7  26581  basellem9  26583  ppiprm  26645  chtprm  26647  musumsum  26686  muinv  26687  logexprlim  26718  perfectlem2  26723  dchrhash  26764  rpvmasum2  27005  slerec  27310  cofcutr  27401  cutlt  27409  addsuniflem  27474  negsunif  27519  ssltmul1  27592  ssltmul2  27593  precsexlem11  27653  axlowdimlem7  28196  axlowdimlem10  28199  upgrex  28342  upgr1elem  28362  uvtxnm1nbgr  28651  umgr2v2e  28772  0oo  30030  sh0le  30681  disjiunel  31815  preimane  31883  fnpreimac  31884  fsuppinisegfi  31897  fprodeq02  32017  s1f1  32097  gsumzresunsn  32194  gsumhashmul  32196  pmtrcnelor  32240  primefldgen1  32400  dvdsrspss  32480  elgrplsmsn  32489  lsmsnorb  32490  grplsm0l  32502  grplsmid  32503  0ringidl  32528  unitpidl1  32531  elrspunsn  32536  drngidl  32540  isprmidlc  32555  qsidomlem2  32561  mxidlprm  32575  mxidlirredi  32576  mxidlirred  32577  drngmxidl  32582  qsdrngilem  32597  lsatdim  32691  drngdimgt0  32692  dimkerim  32701  algextdeglem1  32761  qtopt1  32804  locfinref  32810  zarcls0  32837  zarmxt1  32849  zarcmplem  32850  ordtrestNEW  32890  esumsnf  33051  esum2dlem  33079  rossros  33167  oms0  33285  carsggect  33306  eulerpartlems  33348  eulerpartlemgc  33350  eulerpartlemgh  33366  eulerpartlemgs2  33368  plymulx0  33547  circlemeth  33641  hgt750lemb  33657  hgt750leme  33659  bnj1452  34052  pthhashvtx  34107  subfacp1lem1  34159  subfacp1lem5  34164  erdszelem4  34174  erdszelem8  34178  sconnpi1  34219  cvmscld  34253  cvmlift2lem6  34288  cvmlift2lem9  34291  cvmlift2lem11  34293  cvmlift2lem12  34294  mrsubvrs  34502  gg-dvmulbr  35164  neibastop2lem  35234  topjoin  35239  fnejoin2  35243  pibt2  36287  lindsadd  36470  poimirlem3  36480  poimirlem9  36486  poimirlem28  36505  poimirlem32  36509  prdsbnd  36650  heiborlem8  36675  rrnequiv  36692  grpokerinj  36750  0idl  36882  prnc  36924  isfldidl  36925  lshpnel2N  37844  lsatfixedN  37868  lfl0f  37928  lkrlsp3  37963  elpaddatriN  38663  elpaddat  38664  elpadd2at  38666  pmodlem1  38706  osumcllem1N  38816  osumcllem2N  38817  osumcllem9N  38824  osumcllem10N  38825  pexmidlem6N  38835  pexmidlem7N  38836  dibss  40029  dochocsn  40241  dochsncom  40242  dochnel  40253  dihprrnlem1N  40284  dihprrnlem2  40285  djhlsmat  40287  dihsmsprn  40290  dvh4dimlem  40303  dvhdimlem  40304  dochsnnz  40310  dochsatshp  40311  dochsnshp  40313  dochexmid  40328  dochsnkr  40332  dochsnkr2cl  40334  dochfl1  40336  lcfl7lem  40359  lcfl6  40360  lcfl8  40362  lcfl9a  40365  lclkrlem2a  40367  lclkrlem2c  40369  lclkrlem2d  40370  lclkrlem2e  40371  lclkrlem2j  40376  lclkrlem2o  40381  lclkrlem2p  40382  lclkrlem2s  40385  lclkrlem2v  40388  lcfrlem14  40416  lcfrlem18  40420  lcfrlem19  40421  lcfrlem20  40422  lcfrlem23  40425  lcfrlem25  40427  lcdlkreqN  40482  mapdval4N  40492  mapdsn  40501  mapdhvmap  40629  hdmaprnlem4tN  40712  hdmapinvlem1  40778  hdmapinvlem2  40779  hdmapinvlem3  40780  hdmapinvlem4  40781  hdmapglem5  40782  hgmapvvlem3  40785  hdmapglem7a  40787  hdmapglem7b  40788  hdmapglem7  40789  hdmapoc  40791  sticksstones9  40959  sticksstones11  40961  evlsbagval  41136  selvvvval  41155  0prjspnrel  41366  elrfi  41418  cmpfiiin  41421  mzpcompact2lem  41475  dfac11  41790  pwssplit4  41817  rngunsnply  41901  flcidc  41902  proot1mul  41927  iocinico  41947  cantnfresb  42060  iunrelexp0  42439  frege81d  42484  k0004lem3  42886  mnuunid  43022  binomcxplemnn0  43094  islptre  44322  limciccioolb  44324  limcicciooub  44340  limcresiooub  44345  limcresioolb  44346  ioccncflimc  44588  icccncfext  44590  icocncflimc  44592  cncfiooicc  44597  dvnprodlem2  44650  dirkercncflem2  44807  dirkercncflem3  44808  fourierdlem48  44857  fourierdlem49  44858  fourierdlem79  44888  fourierdlem101  44910  sge0sup  45094  hoidmvlelem2  45299  hoiqssbl  45328  hspmbllem1  45329  hspmbllem2  45330  ovnovollem1  45359  fsumsplitsndif  46028  imaelsetpreimafv  46050  perfectALTVlem2  46377  1hegrlfgr  46497  gsumdifsndf  46578  rnglidl0  46735  sepfsepc  47514