Theorem snssd 4769

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-sn 4586

This theorem is referenced by:  intidg  5412  sofld  6148  fsnex  7240  fr3nr  7728  resf1extb  7890  resf1ext2b  7891  frrlem13  8254  oeeui  8543  naddunif  8634  naddasslem1  8635  naddasslem2  8636  ecinxp  8742  ralxpmap  8846  xpdom3  9016  domunsn  9068  mapdom3  9090  isinf  9183  isinfOLD  9184  ac6sfi  9207  pwfilem  9243  finsschain  9286  ssfii  9346  marypha1lem  9360  unxpwdom2  9517  en2other2  9938  fseqenlem1  9953  axdc3lem4  10382  axdc4lem  10384  ttukeylem7  10444  fpwwe2lem12  10571  canthwe  10580  canthp1lem1  10581  wuncval2  10676  un0addcl  12451  un0mulcl  12452  ssfzunsnext  13506  fseq1p1m1  13535  hashbclem  14393  hashf1lem1  14396  fsumsplit1  15687  fsumge1  15739  incexclem  15778  isumltss  15790  fprodsplit1f  15932  rpnnen2lem11  16168  bitsinv1  16388  lcmfunsnlem2  16586  lcmfass  16592  phicl2  16714  vdwlem1  16928  vdwlem8  16935  vdwlem12  16939  vdwlem13  16940  0ram  16967  ramub1lem1  16973  ramub1lem2  16974  ramcl  16976  imasaddfnlem  17467  imasaddflem  17469  imasvscafn  17476  imasvscaf  17478  mrieqvlemd  17566  mreexmrid  17580  mreexexlem4d  17584  acsfiindd  18488  acsmapd  18489  gsumress  18585  0subm  18720  gsumvallem2  18737  0subgOLD  19060  trivsubgd  19061  trivsubgsnd  19062  trivnsgd  19080  cycsubg2cl  19119  kerf1ghm  19155  pmtrprfv  19359  odf1o1  19478  gex1  19497  sylow2alem1  19523  sylow2alem2  19524  lsm01  19577  lsm02  19578  lsmdisj  19587  lsmdisj2  19588  prmcyg  19800  gsumzadd  19828  gsumconst  19840  gsumdifsnd  19867  gsumpt  19868  gsumxp  19882  dmdprdd  19907  dprdfadd  19928  dprdres  19936  dprdz  19938  dprdsn  19944  dprddisj2  19947  dprd2da  19950  dprd2d2  19952  dmdprdsplit2lem  19953  dpjcntz  19960  dpjdisj  19961  dpjlsm  19962  dpjidcl  19966  ablfacrp  19974  ablfac1eu  19981  pgpfac1lem1  19982  pgpfac1lem3a  19984  pgpfac1lem3  19985  pgpfac1lem5  19987  pgpfaclem2  19990  acsfn1p  20684  lsssn0  20830  lss0ss  20831  lsptpcl  20861  lspsnvsi  20886  lspun0  20893  pwssplit1  20942  lsmpr  20972  lsppr  20976  lspsntri  20980  lspsolvlem  21028  lspsolv  21029  lsppratlem1  21033  lsppratlem3  21035  lsppratlem4  21036  islbs3  21041  lbsextlem4  21047  rnglidl0  21115  rsp1  21123  lidlnz  21128  lidldvgen  21220  mulgrhm2  21364  zndvds  21435  psrlidm  21847  psrridm  21848  mplmonmul  21919  mdetdiaglem  22461  mdetrlin  22465  mdetrsca  22466  mdetrsca2  22467  mdetrlin2  22470  mdetunilem5  22479  mdetunilem9  22483  mdetmul  22486  en2top  22848  rest0  23032  ordtrest  23065  iscnp4  23126  cnconst2  23146  cnpdis  23156  ist1-2  23210  cnt1  23213  dishaus  23245  discmp  23261  cmpcld  23265  conncompid  23294  dis2ndc  23323  dislly  23360  dissnref  23391  comppfsc  23395  llycmpkgen2  23413  cmpkgen  23414  1stckgenlem  23416  1stckgen  23417  ptbasfi  23444  txdis  23495  txdis1cn  23498  txcmplem1  23504  xkohaus  23516  xkoptsub  23517  xkoinjcn  23550  snfbas  23729  trnei  23755  isufil2  23771  ufileu  23782  filufint  23783  uffixsn  23788  ufildom1  23789  flimopn  23838  hausflim  23844  flimcf  23845  flimclslem  23847  flimsncls  23849  cnpflf2  23863  cnpflf  23864  fclsneii  23880  fclsfnflim  23890  fcfnei  23898  flfcntr  23906  alexsubALTlem3  23912  alexsubALTlem4  23913  ptcmplem2  23916  cldsubg  23974  snclseqg  23979  qustgphaus  23986  tsmsgsum  24002  tsmsid  24003  tgptsmscld  24014  tsmsxplem1  24016  tsmsxplem2  24017  ust0  24083  ustuqtop1  24105  neipcfilu  24159  prdsdsf  24231  prdsxmetlem  24232  prdsmet  24234  imasdsf1olem  24237  xpsdsval  24245  prdsbl  24355  prdsxmslem2  24393  idnghm  24607  icccmplem2  24688  metnrmlem2  24725  ioombl  25442  volivth  25484  itg11  25568  i1fmulclem  25579  itg2mulclem  25623  itgsplitioo  25715  limcvallem  25748  limcdif  25753  ellimc2  25754  limcflf  25758  limcmpt2  25761  limcres  25763  cnplimc  25764  limccnp  25768  limccnp2  25769  limcco  25770  dvreslem  25786  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  dvcmulf  25824  dvef  25860  dvivth  25891  lhop2  25896  lhop  25897  ply1remlem  26046  fta1blem  26052  ig1peu  26056  ig1pdvds  26061  plyco0  26073  elply2  26077  plyf  26079  elplyr  26082  elplyd  26083  ply1term  26085  ply0  26089  plyeq0lem  26091  plyeq0  26092  plypf1  26093  plyaddlem  26096  plymullem  26097  dgrlem  26110  coef2  26112  coeidlem  26118  plyco  26122  coemulhi  26135  plycj  26159  plycjOLD  26161  vieta1  26196  taylf  26244  radcnv0  26301  abelth  26327  rlimcnp  26851  xrlimcnp  26854  amgm  26877  wilthlem2  26955  basellem7  26973  basellem9  26975  ppiprm  27037  chtprm  27039  musumsum  27078  muinv  27079  logexprlim  27112  perfectlem2  27117  dchrhash  27158  rpvmasum2  27399  ssltsn  27680  slerec  27707  cofcutr  27808  cutlt  27816  cutmax  27818  cutmin  27819  addsuniflem  27884  negsunif  27937  ssltmul1  28026  ssltmul2  28027  precsexlem11  28095  onscutlt  28141  n0sfincut  28222  0reno  28324  axlowdimlem7  28851  axlowdimlem10  28854  upgrex  28995  upgr1elem  29015  uvtxnm1nbgr  29307  umgr2v2e  29429  cyclnumvtx  29703  0oo  30691  sh0le  31342  disjiunel  32498  preimane  32567  fnpreimac  32568  fsuppinisegfi  32583  fprodeq02  32721  s1f1  32837  gsumzresunsn  32969  gsumhashmul  32974  pmtrcnelor  33021  primefldgen1  33244  dvdsrspss  33331  elgrplsmsn  33334  lsmsnorb  33335  grplsm0l  33347  grplsmid  33348  0ringidl  33365  unitpidl1  33368  elrspunsn  33373  drngidl  33377  isprmidlc  33391  qsidomlem2  33397  ssdifidlprm  33402  mxidlprm  33414  mxidlirredi  33415  mxidlirred  33416  drngmxidl  33421  drngmxidlr  33422  qsdrngilem  33438  rsprprmprmidl  33466  rprmirredb  33476  1arithufdlem4  33491  lsatdim  33586  drngdimgt0  33587  dimkerim  33596  evls1fldgencl  33638  algextdeglem1  33680  algextdeglem2  33681  algextdeglem3  33682  algextdeglem4  33683  algextdeglem5  33684  rtelextdg2  33690  constrextdg2lem  33711  constrext2chnlem  33713  constrfiss  33714  qtopt1  33798  locfinref  33804  zarcls0  33831  zarmxt1  33843  zarcmplem  33844  ordtrestNEW  33884  esumsnf  34027  esum2dlem  34055  rossros  34143  oms0  34261  carsggect  34282  eulerpartlems  34324  eulerpartlemgc  34326  eulerpartlemgh  34342  eulerpartlemgs2  34344  plymulx0  34511  circlemeth  34604  hgt750lemb  34620  hgt750leme  34622  bnj1452  35015  pthhashvtx  35088  subfacp1lem1  35139  subfacp1lem5  35144  erdszelem4  35154  erdszelem8  35158  sconnpi1  35199  cvmscld  35233  cvmlift2lem6  35268  cvmlift2lem9  35271  cvmlift2lem11  35273  cvmlift2lem12  35274  mrsubvrs  35482  ellcsrspsn  35601  neibastop2lem  36321  topjoin  36326  fnejoin2  36330  weiunse  36429  pibt2  37378  lindsadd  37580  poimirlem3  37590  poimirlem9  37596  poimirlem28  37615  poimirlem32  37619  prdsbnd  37760  heiborlem8  37785  rrnequiv  37802  grpokerinj  37860  0idl  37992  prnc  38034  isfldidl  38035  lshpnel2N  38951  lsatfixedN  38975  lfl0f  39035  lkrlsp3  39070  elpaddatriN  39770  elpaddat  39771  elpadd2at  39773  pmodlem1  39813  osumcllem1N  39923  osumcllem2N  39924  osumcllem9N  39931  osumcllem10N  39932  pexmidlem6N  39942  pexmidlem7N  39943  dibss  41136  dochocsn  41348  dochsncom  41349  dochnel  41360  dihprrnlem1N  41391  dihprrnlem2  41392  djhlsmat  41394  dihsmsprn  41397  dvh4dimlem  41410  dvhdimlem  41411  dochsnnz  41417  dochsatshp  41418  dochsnshp  41420  dochexmid  41435  dochsnkr  41439  dochsnkr2cl  41441  dochfl1  41443  lcfl7lem  41466  lcfl6  41467  lcfl8  41469  lcfl9a  41472  lclkrlem2a  41474  lclkrlem2c  41476  lclkrlem2d  41477  lclkrlem2e  41478  lclkrlem2j  41483  lclkrlem2o  41488  lclkrlem2p  41489  lclkrlem2s  41492  lclkrlem2v  41495  lcfrlem14  41523  lcfrlem18  41527  lcfrlem19  41528  lcfrlem20  41529  lcfrlem23  41532  lcfrlem25  41534  lcdlkreqN  41589  mapdval4N  41599  mapdsn  41608  mapdhvmap  41736  hdmaprnlem4tN  41819  hdmapinvlem1  41885  hdmapinvlem2  41886  hdmapinvlem3  41887  hdmapinvlem4  41888  hdmapglem5  41889  hgmapvvlem3  41892  hdmapglem7a  41894  hdmapglem7b  41895  hdmapglem7  41896  hdmapoc  41898  aks6d1c5lem3  42098  deg1gprod  42101  sticksstones9  42115  sticksstones11  42117  rhmqusspan  42146  evlsbagval  42527  selvvvval  42546  0prjspnrel  42588  elrfi  42655  cmpfiiin  42658  mzpcompact2lem  42712  dfac11  43024  pwssplit4  43051  rngunsnply  43131  flcidc  43132  proot1mul  43156  iocinico  43174  cantnfresb  43286  iunrelexp0  43664  frege81d  43709  k0004lem3  44111  mnuunid  44239  binomcxplemnn0  44311  islptre  45590  limciccioolb  45592  limcicciooub  45608  limcresiooub  45613  limcresioolb  45614  ioccncflimc  45856  icccncfext  45858  icocncflimc  45860  cncfiooicc  45865  dvnprodlem2  45918  dirkercncflem2  46075  dirkercncflem3  46076  fourierdlem48  46125  fourierdlem49  46126  fourierdlem79  46156  fourierdlem101  46178  sge0sup  46362  hoidmvlelem2  46567  hoiqssbl  46596  hspmbllem1  46597  hspmbllem2  46598  ovnovollem1  46627  fsumsplitsndif  47347  imaelsetpreimafv  47369  perfectALTVlem2  47696  stgrclnbgr0  47937  isubgr3stgrlem3  47940  1hegrlfgr  48093  gsumdifsndf  48142  sepfsepc  48889  discsubc  49026  iinfconstbas  49028