Theorem snssd 4813

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

Syntax hints:   → wi 4   ∈ wcel 2105   ⊆ wss 3962  {csn 4630

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-ss 3979  df-sn 4631

This theorem is referenced by:  intidg  5467  sofld  6208  fsnex  7302  fr3nr  7790  frrlem13  8321  wfrlem15OLD  8361  oeeui  8638  naddunif  8729  naddasslem1  8730  naddasslem2  8731  ecinxp  8830  ralxpmap  8934  xpdom3  9108  domunsn  9165  mapdom3  9187  isinf  9293  isinfOLD  9294  ac6sfi  9317  pwfilem  9353  finsschain  9396  ssfii  9456  marypha1lem  9470  unxpwdom2  9625  en2other2  10046  fseqenlem1  10061  axdc3lem4  10490  axdc4lem  10492  ttukeylem7  10552  fpwwe2lem12  10679  canthwe  10688  canthp1lem1  10689  wuncval2  10784  un0addcl  12556  un0mulcl  12557  ssfzunsnext  13605  fseq1p1m1  13634  hashbclem  14487  hashf1lem1  14490  fsumsplit1  15777  fsumge1  15829  incexclem  15868  isumltss  15880  fprodsplit1f  16022  rpnnen2lem11  16256  bitsinv1  16475  lcmfunsnlem2  16673  lcmfass  16679  phicl2  16801  vdwlem1  17014  vdwlem8  17021  vdwlem12  17025  vdwlem13  17026  0ram  17053  ramub1lem1  17059  ramub1lem2  17060  ramcl  17062  imasaddfnlem  17574  imasaddflem  17576  imasvscafn  17583  imasvscaf  17585  mrieqvlemd  17673  mreexmrid  17687  mreexexlem4d  17691  acsfiindd  18610  acsmapd  18611  gsumress  18707  0subm  18842  gsumvallem2  18859  0subgOLD  19182  trivsubgd  19183  trivsubgsnd  19184  trivnsgd  19202  cycsubg2cl  19241  kerf1ghm  19277  pmtrprfv  19485  odf1o1  19604  gex1  19623  sylow2alem1  19649  sylow2alem2  19650  lsm01  19703  lsm02  19704  lsmdisj  19713  lsmdisj2  19714  prmcyg  19926  gsumzadd  19954  gsumconst  19966  gsumdifsnd  19993  gsumpt  19994  gsumxp  20008  dmdprdd  20033  dprdfadd  20054  dprdres  20062  dprdz  20064  dprdsn  20070  dprddisj2  20073  dprd2da  20076  dprd2d2  20078  dmdprdsplit2lem  20079  dpjcntz  20086  dpjdisj  20087  dpjlsm  20088  dpjidcl  20092  ablfacrp  20100  ablfac1eu  20107  pgpfac1lem1  20108  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem5  20113  pgpfaclem2  20116  acsfn1p  20816  lsssn0  20963  lss0ss  20964  lsptpcl  20994  lspsnvsi  21019  lspun0  21026  pwssplit1  21075  lsmpr  21105  lsppr  21109  lspsntri  21113  lspsolvlem  21161  lspsolv  21162  lsppratlem1  21166  lsppratlem3  21168  lsppratlem4  21169  islbs3  21174  lbsextlem4  21180  rnglidl0  21256  rsp1  21264  lidlnz  21269  lidldvgen  21361  mulgrhm2  21506  zndvds  21585  psrlidm  21999  psrridm  22000  mplmonmul  22071  mdetdiaglem  22619  mdetrlin  22623  mdetrsca  22624  mdetrsca2  22625  mdetrlin2  22628  mdetunilem5  22637  mdetunilem9  22641  mdetmul  22644  en2top  23007  rest0  23192  ordtrest  23225  iscnp4  23286  cnconst2  23306  cnpdis  23316  ist1-2  23370  cnt1  23373  dishaus  23405  discmp  23421  cmpcld  23425  conncompid  23454  dis2ndc  23483  dislly  23520  dissnref  23551  comppfsc  23555  llycmpkgen2  23573  cmpkgen  23574  1stckgenlem  23576  1stckgen  23577  ptbasfi  23604  txdis  23655  txdis1cn  23658  txcmplem1  23664  xkohaus  23676  xkoptsub  23677  xkoinjcn  23710  snfbas  23889  trnei  23915  isufil2  23931  ufileu  23942  filufint  23943  uffixsn  23948  ufildom1  23949  flimopn  23998  hausflim  24004  flimcf  24005  flimclslem  24007  flimsncls  24009  cnpflf2  24023  cnpflf  24024  fclsneii  24040  fclsfnflim  24050  fcfnei  24058  flfcntr  24066  alexsubALTlem3  24072  alexsubALTlem4  24073  ptcmplem2  24076  cldsubg  24134  snclseqg  24139  qustgphaus  24146  tsmsgsum  24162  tsmsid  24163  tgptsmscld  24174  tsmsxplem1  24176  tsmsxplem2  24177  ust0  24243  ustuqtop1  24265  neipcfilu  24320  prdsdsf  24392  prdsxmetlem  24393  prdsmet  24395  imasdsf1olem  24398  xpsdsval  24406  prdsbl  24519  prdsxmslem2  24557  idnghm  24779  icccmplem2  24858  metnrmlem2  24895  ioombl  25613  volivth  25655  itg11  25739  i1fmulclem  25751  itg2mulclem  25795  itgsplitioo  25887  limcvallem  25920  limcdif  25925  ellimc2  25926  limcflf  25930  limcmpt2  25933  limcres  25935  cnplimc  25936  limccnp  25940  limccnp2  25941  limcco  25942  dvreslem  25958  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvcmulf  25996  dvef  26032  dvivth  26063  lhop2  26068  lhop  26069  ply1remlem  26218  fta1blem  26224  ig1peu  26228  ig1pdvds  26233  plyco0  26245  elply2  26249  plyf  26251  elplyr  26254  elplyd  26255  ply1term  26257  ply0  26261  plyeq0lem  26263  plyeq0  26264  plypf1  26265  plyaddlem  26268  plymullem  26269  dgrlem  26282  coef2  26284  coeidlem  26290  plyco  26294  coemulhi  26307  plycj  26331  plycjOLD  26333  vieta1  26368  taylf  26416  radcnv0  26473  abelth  26499  rlimcnp  27022  xrlimcnp  27025  amgm  27048  wilthlem2  27126  basellem7  27144  basellem9  27146  ppiprm  27208  chtprm  27210  musumsum  27249  muinv  27250  logexprlim  27283  perfectlem2  27288  dchrhash  27329  rpvmasum2  27570  ssltsn  27851  slerec  27878  cofcutr  27972  cutlt  27980  cutmax  27982  cutmin  27983  addsuniflem  28048  negsunif  28101  ssltmul1  28187  ssltmul2  28188  precsexlem11  28255  nohalf  28421  0reno  28443  axlowdimlem7  28977  axlowdimlem10  28980  upgrex  29123  upgr1elem  29143  uvtxnm1nbgr  29435  umgr2v2e  29557  0oo  30817  sh0le  31468  disjiunel  32615  preimane  32686  fnpreimac  32687  fsuppinisegfi  32701  fprodeq02  32829  s1f1  32911  gsumzresunsn  33041  gsumhashmul  33046  pmtrcnelor  33093  primefldgen1  33302  dvdsrspss  33394  elgrplsmsn  33397  lsmsnorb  33398  grplsm0l  33410  grplsmid  33411  0ringidl  33428  unitpidl1  33431  elrspunsn  33436  drngidl  33440  isprmidlc  33454  qsidomlem2  33460  ssdifidlprm  33465  mxidlprm  33477  mxidlirredi  33478  mxidlirred  33479  drngmxidl  33484  drngmxidlr  33485  qsdrngilem  33501  rsprprmprmidl  33529  rprmirredb  33539  1arithufdlem4  33554  lsatdim  33644  drngdimgt0  33645  dimkerim  33654  evls1fldgencl  33694  algextdeglem1  33722  algextdeglem2  33723  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  rtelextdg2  33732  qtopt1  33795  locfinref  33801  zarcls0  33828  zarmxt1  33840  zarcmplem  33841  ordtrestNEW  33881  esumsnf  34044  esum2dlem  34072  rossros  34160  oms0  34278  carsggect  34299  eulerpartlems  34341  eulerpartlemgc  34343  eulerpartlemgh  34359  eulerpartlemgs2  34361  plymulx0  34540  circlemeth  34633  hgt750lemb  34649  hgt750leme  34651  bnj1452  35044  pthhashvtx  35111  subfacp1lem1  35163  subfacp1lem5  35168  erdszelem4  35178  erdszelem8  35182  sconnpi1  35223  cvmscld  35257  cvmlift2lem6  35292  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift2lem12  35298  mrsubvrs  35506  ellcsrspsn  35625  neibastop2lem  36342  topjoin  36347  fnejoin2  36351  weiunse  36450  pibt2  37399  lindsadd  37599  poimirlem3  37609  poimirlem9  37615  poimirlem28  37634  poimirlem32  37638  prdsbnd  37779  heiborlem8  37804  rrnequiv  37821  grpokerinj  37879  0idl  38011  prnc  38053  isfldidl  38054  lshpnel2N  38966  lsatfixedN  38990  lfl0f  39050  lkrlsp3  39085  elpaddatriN  39785  elpaddat  39786  elpadd2at  39788  pmodlem1  39828  osumcllem1N  39938  osumcllem2N  39939  osumcllem9N  39946  osumcllem10N  39947  pexmidlem6N  39957  pexmidlem7N  39958  dibss  41151  dochocsn  41363  dochsncom  41364  dochnel  41375  dihprrnlem1N  41406  dihprrnlem2  41407  djhlsmat  41409  dihsmsprn  41412  dvh4dimlem  41425  dvhdimlem  41426  dochsnnz  41432  dochsatshp  41433  dochsnshp  41435  dochexmid  41450  dochsnkr  41454  dochsnkr2cl  41456  dochfl1  41458  lcfl7lem  41481  lcfl6  41482  lcfl8  41484  lcfl9a  41487  lclkrlem2a  41489  lclkrlem2c  41491  lclkrlem2d  41492  lclkrlem2e  41493  lclkrlem2j  41498  lclkrlem2o  41503  lclkrlem2p  41504  lclkrlem2s  41507  lclkrlem2v  41510  lcfrlem14  41538  lcfrlem18  41542  lcfrlem19  41543  lcfrlem20  41544  lcfrlem23  41547  lcfrlem25  41549  lcdlkreqN  41604  mapdval4N  41614  mapdsn  41623  mapdhvmap  41751  hdmaprnlem4tN  41834  hdmapinvlem1  41900  hdmapinvlem2  41901  hdmapinvlem3  41902  hdmapinvlem4  41903  hdmapglem5  41904  hgmapvvlem3  41907  hdmapglem7a  41909  hdmapglem7b  41910  hdmapglem7  41911  hdmapoc  41913  aks6d1c5lem3  42118  deg1gprod  42121  sticksstones9  42135  sticksstones11  42137  rhmqusspan  42166  evlsbagval  42552  selvvvval  42571  0prjspnrel  42613  elrfi  42681  cmpfiiin  42684  mzpcompact2lem  42738  dfac11  43050  pwssplit4  43077  rngunsnply  43157  flcidc  43158  proot1mul  43182  iocinico  43200  cantnfresb  43313  iunrelexp0  43691  frege81d  43736  k0004lem3  44138  mnuunid  44272  binomcxplemnn0  44344  islptre  45574  limciccioolb  45576  limcicciooub  45592  limcresiooub  45597  limcresioolb  45598  ioccncflimc  45840  icccncfext  45842  icocncflimc  45844  cncfiooicc  45849  dvnprodlem2  45902  dirkercncflem2  46059  dirkercncflem3  46060  fourierdlem48  46109  fourierdlem49  46110  fourierdlem79  46140  fourierdlem101  46162  sge0sup  46346  hoidmvlelem2  46551  hoiqssbl  46580  hspmbllem1  46581  hspmbllem2  46582  ovnovollem1  46611  fsumsplitsndif  47297  imaelsetpreimafv  47319  perfectALTVlem2  47646  stgrclnbgr0  47867  isubgr3stgrlem3  47870  1hegrlfgr  47975  gsumdifsndf  48024  sepfsepc  48723