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 2104   ⊆ wss 3949  {csn 4629

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3956  df-ss 3966  df-sn 4630

This theorem is referenced by:  intidg  5458  sofld  6187  fsnex  7285  fr3nr  7763  frrlem13  8287  wfrlem15OLD  8327  oeeui  8606  naddunif  8696  naddasslem1  8697  naddasslem2  8698  ecinxp  8790  ralxpmap  8894  xpdom3  9074  domunsn  9131  mapdom3  9153  pwfilem  9181  isinf  9264  isinfOLD  9265  ac6sfi  9291  pwfilemOLD  9350  finsschain  9363  ssfii  9418  marypha1lem  9432  unxpwdom2  9587  en2other2  10008  fseqenlem1  10023  axdc3lem4  10452  axdc4lem  10454  ttukeylem7  10514  fpwwe2lem12  10641  canthwe  10650  canthp1lem1  10651  wuncval2  10746  un0addcl  12511  un0mulcl  12512  ssfzunsnext  13552  fseq1p1m1  13581  hashbclem  14417  hashf1lem1  14421  hashf1lem1OLD  14422  fsumsplit1  15697  fsumge1  15749  incexclem  15788  isumltss  15800  fprodsplit1f  15940  rpnnen2lem11  16173  bitsinv1  16389  lcmfunsnlem2  16583  lcmfass  16589  phicl2  16707  vdwlem1  16920  vdwlem8  16927  vdwlem12  16931  vdwlem13  16932  0ram  16959  ramub1lem1  16965  ramub1lem2  16966  ramcl  16968  imasaddfnlem  17480  imasaddflem  17482  imasvscafn  17489  imasvscaf  17491  mrieqvlemd  17579  mreexmrid  17593  mreexexlem4d  17597  acsfiindd  18512  acsmapd  18513  gsumress  18609  0subm  18736  gsumvallem2  18753  0subgOLD  19070  trivsubgd  19071  trivsubgsnd  19072  trivnsgd  19090  cycsubg2cl  19128  kerf1ghm  19163  pmtrprfv  19364  odf1o1  19483  gex1  19502  sylow2alem1  19528  sylow2alem2  19529  lsm01  19582  lsm02  19583  lsmdisj  19592  lsmdisj2  19593  prmcyg  19805  gsumzadd  19833  gsumconst  19845  gsumdifsnd  19872  gsumpt  19873  gsumxp  19887  dmdprdd  19912  dprdfadd  19933  dprdres  19941  dprdz  19943  dprdsn  19949  dprddisj2  19952  dprd2da  19955  dprd2d2  19957  dmdprdsplit2lem  19958  dpjcntz  19965  dpjdisj  19966  dpjlsm  19967  dpjidcl  19971  ablfacrp  19979  ablfac1eu  19986  pgpfac1lem1  19987  pgpfac1lem3a  19989  pgpfac1lem3  19990  pgpfac1lem5  19992  pgpfaclem2  19995  acsfn1p  20560  lsssn0  20704  lss0ss  20705  lsptpcl  20736  lspsnvsi  20761  lspun0  20768  pwssplit1  20816  lsmpr  20846  lsppr  20850  lspsntri  20854  lspsolvlem  20902  lspsolv  20903  lsppratlem1  20907  lsppratlem3  20909  lsppratlem4  20910  islbs3  20915  lbsextlem4  20921  rsp1  21000  lidlnz  21004  rnglidl0  21034  lidldvgen  21095  mulgrhm2  21251  zndvds  21326  psrlidm  21744  psrridm  21745  mplmonmul  21812  mdetdiaglem  22322  mdetrlin  22326  mdetrsca  22327  mdetrsca2  22328  mdetrlin2  22331  mdetunilem5  22340  mdetunilem9  22344  mdetmul  22347  en2top  22710  rest0  22895  ordtrest  22928  iscnp4  22989  cnconst2  23009  cnpdis  23019  ist1-2  23073  cnt1  23076  dishaus  23108  discmp  23124  cmpcld  23128  conncompid  23157  dis2ndc  23186  dislly  23223  dissnref  23254  comppfsc  23258  llycmpkgen2  23276  cmpkgen  23277  1stckgenlem  23279  1stckgen  23280  ptbasfi  23307  txdis  23358  txdis1cn  23361  txcmplem1  23367  xkohaus  23379  xkoptsub  23380  xkoinjcn  23413  snfbas  23592  trnei  23618  isufil2  23634  ufileu  23645  filufint  23646  uffixsn  23651  ufildom1  23652  flimopn  23701  hausflim  23707  flimcf  23708  flimclslem  23710  flimsncls  23712  cnpflf2  23726  cnpflf  23727  fclsneii  23743  fclsfnflim  23753  fcfnei  23761  flfcntr  23769  alexsubALTlem3  23775  alexsubALTlem4  23776  ptcmplem2  23779  cldsubg  23837  snclseqg  23842  qustgphaus  23849  tsmsgsum  23865  tsmsid  23866  tgptsmscld  23877  tsmsxplem1  23879  tsmsxplem2  23880  ust0  23946  ustuqtop1  23968  neipcfilu  24023  prdsdsf  24095  prdsxmetlem  24096  prdsmet  24098  imasdsf1olem  24101  xpsdsval  24109  prdsbl  24222  prdsxmslem2  24260  idnghm  24482  icccmplem2  24561  metnrmlem2  24598  ioombl  25316  volivth  25358  itg11  25442  i1fmulclem  25454  itg2mulclem  25498  itgsplitioo  25589  limcvallem  25622  limcdif  25627  ellimc2  25628  limcflf  25632  limcmpt2  25635  limcres  25637  cnplimc  25638  limccnp  25642  limccnp2  25643  limcco  25644  dvreslem  25660  dvaddbr  25689  dvmulbr  25690  dvcmulf  25696  dvef  25731  dvivth  25761  lhop2  25766  lhop  25767  ply1remlem  25914  fta1blem  25920  ig1peu  25923  ig1pdvds  25928  plyco0  25940  elply2  25944  plyf  25946  elplyr  25949  elplyd  25950  ply1term  25952  ply0  25956  plyeq0lem  25958  plyeq0  25959  plypf1  25960  plyaddlem  25963  plymullem  25964  dgrlem  25977  coef2  25979  coeidlem  25985  plyco  25989  coemulhi  26002  plycj  26025  vieta1  26059  taylf  26107  radcnv0  26162  abelth  26187  rlimcnp  26704  xrlimcnp  26707  amgm  26729  wilthlem2  26807  basellem7  26825  basellem9  26827  ppiprm  26889  chtprm  26891  musumsum  26930  muinv  26931  logexprlim  26962  perfectlem2  26967  dchrhash  27008  rpvmasum2  27249  ssltsn  27528  slerec  27555  cofcutr  27647  cutlt  27655  addsuniflem  27721  negsunif  27766  ssltmul1  27839  ssltmul2  27840  precsexlem11  27900  axlowdimlem7  28471  axlowdimlem10  28474  upgrex  28617  upgr1elem  28637  uvtxnm1nbgr  28926  umgr2v2e  29047  0oo  30307  sh0le  30958  disjiunel  32092  preimane  32160  fnpreimac  32161  fsuppinisegfi  32174  fprodeq02  32294  s1f1  32374  gsumzresunsn  32474  gsumhashmul  32476  pmtrcnelor  32520  primefldgen1  32679  dvdsrspss  32763  elgrplsmsn  32772  lsmsnorb  32773  grplsm0l  32785  grplsmid  32786  0ringidl  32811  unitpidl1  32814  elrspunsn  32819  drngidl  32823  isprmidlc  32838  qsidomlem2  32844  mxidlprm  32858  mxidlirredi  32859  mxidlirred  32860  drngmxidl  32865  qsdrngilem  32880  lsatdim  32988  drngdimgt0  32989  dimkerim  32998  evls1fldgencl  33031  algextdeglem1  33060  algextdeglem2  33061  algextdeglem3  33062  algextdeglem4  33063  algextdeglem5  33064  qtopt1  33111  locfinref  33117  zarcls0  33144  zarmxt1  33156  zarcmplem  33157  ordtrestNEW  33197  esumsnf  33358  esum2dlem  33386  rossros  33474  oms0  33592  carsggect  33613  eulerpartlems  33655  eulerpartlemgc  33657  eulerpartlemgh  33673  eulerpartlemgs2  33675  plymulx0  33854  circlemeth  33948  hgt750lemb  33964  hgt750leme  33966  bnj1452  34359  pthhashvtx  34414  subfacp1lem1  34466  subfacp1lem5  34471  erdszelem4  34481  erdszelem8  34485  sconnpi1  34526  cvmscld  34560  cvmlift2lem6  34595  cvmlift2lem9  34598  cvmlift2lem11  34600  cvmlift2lem12  34601  mrsubvrs  34809  gg-dvmulbr  35463  neibastop2lem  35550  topjoin  35555  fnejoin2  35559  pibt2  36603  lindsadd  36786  poimirlem3  36796  poimirlem9  36802  poimirlem28  36821  poimirlem32  36825  prdsbnd  36966  heiborlem8  36991  rrnequiv  37008  grpokerinj  37066  0idl  37198  prnc  37240  isfldidl  37241  lshpnel2N  38160  lsatfixedN  38184  lfl0f  38244  lkrlsp3  38279  elpaddatriN  38979  elpaddat  38980  elpadd2at  38982  pmodlem1  39022  osumcllem1N  39132  osumcllem2N  39133  osumcllem9N  39140  osumcllem10N  39141  pexmidlem6N  39151  pexmidlem7N  39152  dibss  40345  dochocsn  40557  dochsncom  40558  dochnel  40569  dihprrnlem1N  40600  dihprrnlem2  40601  djhlsmat  40603  dihsmsprn  40606  dvh4dimlem  40619  dvhdimlem  40620  dochsnnz  40626  dochsatshp  40627  dochsnshp  40629  dochexmid  40644  dochsnkr  40648  dochsnkr2cl  40650  dochfl1  40652  lcfl7lem  40675  lcfl6  40676  lcfl8  40678  lcfl9a  40681  lclkrlem2a  40683  lclkrlem2c  40685  lclkrlem2d  40686  lclkrlem2e  40687  lclkrlem2j  40692  lclkrlem2o  40697  lclkrlem2p  40698  lclkrlem2s  40701  lclkrlem2v  40704  lcfrlem14  40732  lcfrlem18  40736  lcfrlem19  40737  lcfrlem20  40738  lcfrlem23  40741  lcfrlem25  40743  lcdlkreqN  40798  mapdval4N  40808  mapdsn  40817  mapdhvmap  40945  hdmaprnlem4tN  41028  hdmapinvlem1  41094  hdmapinvlem2  41095  hdmapinvlem3  41096  hdmapinvlem4  41097  hdmapglem5  41098  hgmapvvlem3  41101  hdmapglem7a  41103  hdmapglem7b  41104  hdmapglem7  41105  hdmapoc  41107  sticksstones9  41278  sticksstones11  41280  evlsbagval  41442  selvvvval  41461  0prjspnrel  41673  elrfi  41736  cmpfiiin  41739  mzpcompact2lem  41793  dfac11  42108  pwssplit4  42135  rngunsnply  42219  flcidc  42220  proot1mul  42245  iocinico  42265  cantnfresb  42378  iunrelexp0  42757  frege81d  42802  k0004lem3  43204  mnuunid  43340  binomcxplemnn0  43412  islptre  44635  limciccioolb  44637  limcicciooub  44653  limcresiooub  44658  limcresioolb  44659  ioccncflimc  44901  icccncfext  44903  icocncflimc  44905  cncfiooicc  44910  dvnprodlem2  44963  dirkercncflem2  45120  dirkercncflem3  45121  fourierdlem48  45170  fourierdlem49  45171  fourierdlem79  45201  fourierdlem101  45223  sge0sup  45407  hoidmvlelem2  45612  hoiqssbl  45641  hspmbllem1  45642  hspmbllem2  45643  ovnovollem1  45672  fsumsplitsndif  46341  imaelsetpreimafv  46363  perfectALTVlem2  46690  1hegrlfgr  46810  gsumdifsndf  46859  sepfsepc  47649