Theorem snssd 4834

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3976  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-ss 3993  df-sn 4649

This theorem is referenced by:  intidg  5477  sofld  6218  fsnex  7319  fr3nr  7807  frrlem13  8339  wfrlem15OLD  8379  oeeui  8658  naddunif  8749  naddasslem1  8750  naddasslem2  8751  ecinxp  8850  ralxpmap  8954  xpdom3  9136  domunsn  9193  mapdom3  9215  isinf  9323  isinfOLD  9324  ac6sfi  9348  pwfilem  9384  pwfilemOLD  9416  finsschain  9429  ssfii  9488  marypha1lem  9502  unxpwdom2  9657  en2other2  10078  fseqenlem1  10093  axdc3lem4  10522  axdc4lem  10524  ttukeylem7  10584  fpwwe2lem12  10711  canthwe  10720  canthp1lem1  10721  wuncval2  10816  un0addcl  12586  un0mulcl  12587  ssfzunsnext  13629  fseq1p1m1  13658  hashbclem  14501  hashf1lem1  14504  fsumsplit1  15793  fsumge1  15845  incexclem  15884  isumltss  15896  fprodsplit1f  16038  rpnnen2lem11  16272  bitsinv1  16488  lcmfunsnlem2  16687  lcmfass  16693  phicl2  16815  vdwlem1  17028  vdwlem8  17035  vdwlem12  17039  vdwlem13  17040  0ram  17067  ramub1lem1  17073  ramub1lem2  17074  ramcl  17076  imasaddfnlem  17588  imasaddflem  17590  imasvscafn  17597  imasvscaf  17599  mrieqvlemd  17687  mreexmrid  17701  mreexexlem4d  17705  acsfiindd  18623  acsmapd  18624  gsumress  18720  0subm  18852  gsumvallem2  18869  0subgOLD  19192  trivsubgd  19193  trivsubgsnd  19194  trivnsgd  19212  cycsubg2cl  19251  kerf1ghm  19287  pmtrprfv  19495  odf1o1  19614  gex1  19633  sylow2alem1  19659  sylow2alem2  19660  lsm01  19713  lsm02  19714  lsmdisj  19723  lsmdisj2  19724  prmcyg  19936  gsumzadd  19964  gsumconst  19976  gsumdifsnd  20003  gsumpt  20004  gsumxp  20018  dmdprdd  20043  dprdfadd  20064  dprdres  20072  dprdz  20074  dprdsn  20080  dprddisj2  20083  dprd2da  20086  dprd2d2  20088  dmdprdsplit2lem  20089  dpjcntz  20096  dpjdisj  20097  dpjlsm  20098  dpjidcl  20102  ablfacrp  20110  ablfac1eu  20117  pgpfac1lem1  20118  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfac1lem5  20123  pgpfaclem2  20126  acsfn1p  20822  lsssn0  20969  lss0ss  20970  lsptpcl  21000  lspsnvsi  21025  lspun0  21032  pwssplit1  21081  lsmpr  21111  lsppr  21115  lspsntri  21119  lspsolvlem  21167  lspsolv  21168  lsppratlem1  21172  lsppratlem3  21174  lsppratlem4  21175  islbs3  21180  lbsextlem4  21186  rnglidl0  21262  rsp1  21270  lidlnz  21275  lidldvgen  21367  mulgrhm2  21512  zndvds  21591  psrlidm  22005  psrridm  22006  mplmonmul  22077  mdetdiaglem  22625  mdetrlin  22629  mdetrsca  22630  mdetrsca2  22631  mdetrlin2  22634  mdetunilem5  22643  mdetunilem9  22647  mdetmul  22650  en2top  23013  rest0  23198  ordtrest  23231  iscnp4  23292  cnconst2  23312  cnpdis  23322  ist1-2  23376  cnt1  23379  dishaus  23411  discmp  23427  cmpcld  23431  conncompid  23460  dis2ndc  23489  dislly  23526  dissnref  23557  comppfsc  23561  llycmpkgen2  23579  cmpkgen  23580  1stckgenlem  23582  1stckgen  23583  ptbasfi  23610  txdis  23661  txdis1cn  23664  txcmplem1  23670  xkohaus  23682  xkoptsub  23683  xkoinjcn  23716  snfbas  23895  trnei  23921  isufil2  23937  ufileu  23948  filufint  23949  uffixsn  23954  ufildom1  23955  flimopn  24004  hausflim  24010  flimcf  24011  flimclslem  24013  flimsncls  24015  cnpflf2  24029  cnpflf  24030  fclsneii  24046  fclsfnflim  24056  fcfnei  24064  flfcntr  24072  alexsubALTlem3  24078  alexsubALTlem4  24079  ptcmplem2  24082  cldsubg  24140  snclseqg  24145  qustgphaus  24152  tsmsgsum  24168  tsmsid  24169  tgptsmscld  24180  tsmsxplem1  24182  tsmsxplem2  24183  ust0  24249  ustuqtop1  24271  neipcfilu  24326  prdsdsf  24398  prdsxmetlem  24399  prdsmet  24401  imasdsf1olem  24404  xpsdsval  24412  prdsbl  24525  prdsxmslem2  24563  idnghm  24785  icccmplem2  24864  metnrmlem2  24901  ioombl  25619  volivth  25661  itg11  25745  i1fmulclem  25757  itg2mulclem  25801  itgsplitioo  25893  limcvallem  25926  limcdif  25931  ellimc2  25932  limcflf  25936  limcmpt2  25939  limcres  25941  cnplimc  25942  limccnp  25946  limccnp2  25947  limcco  25948  dvreslem  25964  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvcmulf  26002  dvef  26038  dvivth  26069  lhop2  26074  lhop  26075  ply1remlem  26224  fta1blem  26230  ig1peu  26234  ig1pdvds  26239  plyco0  26251  elply2  26255  plyf  26257  elplyr  26260  elplyd  26261  ply1term  26263  ply0  26267  plyeq0lem  26269  plyeq0  26270  plypf1  26271  plyaddlem  26274  plymullem  26275  dgrlem  26288  coef2  26290  coeidlem  26296  plyco  26300  coemulhi  26313  plycj  26337  vieta1  26372  taylf  26420  radcnv0  26477  abelth  26503  rlimcnp  27026  xrlimcnp  27029  amgm  27052  wilthlem2  27130  basellem7  27148  basellem9  27150  ppiprm  27212  chtprm  27214  musumsum  27253  muinv  27254  logexprlim  27287  perfectlem2  27292  dchrhash  27333  rpvmasum2  27574  ssltsn  27855  slerec  27882  cofcutr  27976  cutlt  27984  cutmax  27986  cutmin  27987  addsuniflem  28052  negsunif  28105  ssltmul1  28191  ssltmul2  28192  precsexlem11  28259  nohalf  28425  0reno  28447  axlowdimlem7  28981  axlowdimlem10  28984  upgrex  29127  upgr1elem  29147  uvtxnm1nbgr  29439  umgr2v2e  29561  0oo  30821  sh0le  31472  disjiunel  32618  preimane  32688  fnpreimac  32689  fsuppinisegfi  32699  fprodeq02  32827  s1f1  32909  gsumzresunsn  33037  gsumhashmul  33040  pmtrcnelor  33084  primefldgen1  33288  dvdsrspss  33380  elgrplsmsn  33383  lsmsnorb  33384  grplsm0l  33396  grplsmid  33397  0ringidl  33414  unitpidl1  33417  elrspunsn  33422  drngidl  33426  isprmidlc  33440  qsidomlem2  33446  ssdifidlprm  33451  mxidlprm  33463  mxidlirredi  33464  mxidlirred  33465  drngmxidl  33470  drngmxidlr  33471  qsdrngilem  33487  rsprprmprmidl  33515  rprmirredb  33525  1arithufdlem4  33540  lsatdim  33630  drngdimgt0  33631  dimkerim  33640  evls1fldgencl  33680  algextdeglem1  33708  algextdeglem2  33709  algextdeglem3  33710  algextdeglem4  33711  algextdeglem5  33712  rtelextdg2  33718  qtopt1  33781  locfinref  33787  zarcls0  33814  zarmxt1  33826  zarcmplem  33827  ordtrestNEW  33867  esumsnf  34028  esum2dlem  34056  rossros  34144  oms0  34262  carsggect  34283  eulerpartlems  34325  eulerpartlemgc  34327  eulerpartlemgh  34343  eulerpartlemgs2  34345  plymulx0  34524  circlemeth  34617  hgt750lemb  34633  hgt750leme  34635  bnj1452  35028  pthhashvtx  35095  subfacp1lem1  35147  subfacp1lem5  35152  erdszelem4  35162  erdszelem8  35166  sconnpi1  35207  cvmscld  35241  cvmlift2lem6  35276  cvmlift2lem9  35279  cvmlift2lem11  35281  cvmlift2lem12  35282  mrsubvrs  35490  ellcsrspsn  35609  neibastop2lem  36326  topjoin  36331  fnejoin2  36335  weiunse  36434  pibt2  37383  lindsadd  37573  poimirlem3  37583  poimirlem9  37589  poimirlem28  37608  poimirlem32  37612  prdsbnd  37753  heiborlem8  37778  rrnequiv  37795  grpokerinj  37853  0idl  37985  prnc  38027  isfldidl  38028  lshpnel2N  38941  lsatfixedN  38965  lfl0f  39025  lkrlsp3  39060  elpaddatriN  39760  elpaddat  39761  elpadd2at  39763  pmodlem1  39803  osumcllem1N  39913  osumcllem2N  39914  osumcllem9N  39921  osumcllem10N  39922  pexmidlem6N  39932  pexmidlem7N  39933  dibss  41126  dochocsn  41338  dochsncom  41339  dochnel  41350  dihprrnlem1N  41381  dihprrnlem2  41382  djhlsmat  41384  dihsmsprn  41387  dvh4dimlem  41400  dvhdimlem  41401  dochsnnz  41407  dochsatshp  41408  dochsnshp  41410  dochexmid  41425  dochsnkr  41429  dochsnkr2cl  41431  dochfl1  41433  lcfl7lem  41456  lcfl6  41457  lcfl8  41459  lcfl9a  41462  lclkrlem2a  41464  lclkrlem2c  41466  lclkrlem2d  41467  lclkrlem2e  41468  lclkrlem2j  41473  lclkrlem2o  41478  lclkrlem2p  41479  lclkrlem2s  41482  lclkrlem2v  41485  lcfrlem14  41513  lcfrlem18  41517  lcfrlem19  41518  lcfrlem20  41519  lcfrlem23  41522  lcfrlem25  41524  lcdlkreqN  41579  mapdval4N  41589  mapdsn  41598  mapdhvmap  41726  hdmaprnlem4tN  41809  hdmapinvlem1  41875  hdmapinvlem2  41876  hdmapinvlem3  41877  hdmapinvlem4  41878  hdmapglem5  41879  hgmapvvlem3  41882  hdmapglem7a  41884  hdmapglem7b  41885  hdmapglem7  41886  hdmapoc  41888  aks6d1c5lem3  42094  deg1gprod  42097  sticksstones9  42111  sticksstones11  42113  rhmqusspan  42142  evlsbagval  42521  selvvvval  42540  0prjspnrel  42582  elrfi  42650  cmpfiiin  42653  mzpcompact2lem  42707  dfac11  43019  pwssplit4  43046  rngunsnply  43130  flcidc  43131  proot1mul  43155  iocinico  43173  cantnfresb  43286  iunrelexp0  43664  frege81d  43709  k0004lem3  44111  mnuunid  44246  binomcxplemnn0  44318  islptre  45540  limciccioolb  45542  limcicciooub  45558  limcresiooub  45563  limcresioolb  45564  ioccncflimc  45806  icccncfext  45808  icocncflimc  45810  cncfiooicc  45815  dvnprodlem2  45868  dirkercncflem2  46025  dirkercncflem3  46026  fourierdlem48  46075  fourierdlem49  46076  fourierdlem79  46106  fourierdlem101  46128  sge0sup  46312  hoidmvlelem2  46517  hoiqssbl  46546  hspmbllem1  46547  hspmbllem2  46548  ovnovollem1  46577  fsumsplitsndif  47247  imaelsetpreimafv  47269  perfectALTVlem2  47596  1hegrlfgr  47855  gsumdifsndf  47904  sepfsepc  48607