Theorem snssd 4809

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

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3951  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-ss 3968  df-sn 4627

This theorem is referenced by:  intidg  5462  sofld  6207  fsnex  7303  fr3nr  7792  resf1extb  7956  resf1ext2b  7957  frrlem13  8323  wfrlem15OLD  8363  oeeui  8640  naddunif  8731  naddasslem1  8732  naddasslem2  8733  ecinxp  8832  ralxpmap  8936  xpdom3  9110  domunsn  9167  mapdom3  9189  isinf  9296  isinfOLD  9297  ac6sfi  9320  pwfilem  9356  finsschain  9399  ssfii  9459  marypha1lem  9473  unxpwdom2  9628  en2other2  10049  fseqenlem1  10064  axdc3lem4  10493  axdc4lem  10495  ttukeylem7  10555  fpwwe2lem12  10682  canthwe  10691  canthp1lem1  10692  wuncval2  10787  un0addcl  12559  un0mulcl  12560  ssfzunsnext  13609  fseq1p1m1  13638  hashbclem  14491  hashf1lem1  14494  fsumsplit1  15781  fsumge1  15833  incexclem  15872  isumltss  15884  fprodsplit1f  16026  rpnnen2lem11  16260  bitsinv1  16479  lcmfunsnlem2  16677  lcmfass  16683  phicl2  16805  vdwlem1  17019  vdwlem8  17026  vdwlem12  17030  vdwlem13  17031  0ram  17058  ramub1lem1  17064  ramub1lem2  17065  ramcl  17067  imasaddfnlem  17573  imasaddflem  17575  imasvscafn  17582  imasvscaf  17584  mrieqvlemd  17672  mreexmrid  17686  mreexexlem4d  17690  acsfiindd  18598  acsmapd  18599  gsumress  18695  0subm  18830  gsumvallem2  18847  0subgOLD  19170  trivsubgd  19171  trivsubgsnd  19172  trivnsgd  19190  cycsubg2cl  19229  kerf1ghm  19265  pmtrprfv  19471  odf1o1  19590  gex1  19609  sylow2alem1  19635  sylow2alem2  19636  lsm01  19689  lsm02  19690  lsmdisj  19699  lsmdisj2  19700  prmcyg  19912  gsumzadd  19940  gsumconst  19952  gsumdifsnd  19979  gsumpt  19980  gsumxp  19994  dmdprdd  20019  dprdfadd  20040  dprdres  20048  dprdz  20050  dprdsn  20056  dprddisj2  20059  dprd2da  20062  dprd2d2  20064  dmdprdsplit2lem  20065  dpjcntz  20072  dpjdisj  20073  dpjlsm  20074  dpjidcl  20078  ablfacrp  20086  ablfac1eu  20093  pgpfac1lem1  20094  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem5  20099  pgpfaclem2  20102  acsfn1p  20800  lsssn0  20946  lss0ss  20947  lsptpcl  20977  lspsnvsi  21002  lspun0  21009  pwssplit1  21058  lsmpr  21088  lsppr  21092  lspsntri  21096  lspsolvlem  21144  lspsolv  21145  lsppratlem1  21149  lsppratlem3  21151  lsppratlem4  21152  islbs3  21157  lbsextlem4  21163  rnglidl0  21239  rsp1  21247  lidlnz  21252  lidldvgen  21344  mulgrhm2  21489  zndvds  21568  psrlidm  21982  psrridm  21983  mplmonmul  22054  mdetdiaglem  22604  mdetrlin  22608  mdetrsca  22609  mdetrsca2  22610  mdetrlin2  22613  mdetunilem5  22622  mdetunilem9  22626  mdetmul  22629  en2top  22992  rest0  23177  ordtrest  23210  iscnp4  23271  cnconst2  23291  cnpdis  23301  ist1-2  23355  cnt1  23358  dishaus  23390  discmp  23406  cmpcld  23410  conncompid  23439  dis2ndc  23468  dislly  23505  dissnref  23536  comppfsc  23540  llycmpkgen2  23558  cmpkgen  23559  1stckgenlem  23561  1stckgen  23562  ptbasfi  23589  txdis  23640  txdis1cn  23643  txcmplem1  23649  xkohaus  23661  xkoptsub  23662  xkoinjcn  23695  snfbas  23874  trnei  23900  isufil2  23916  ufileu  23927  filufint  23928  uffixsn  23933  ufildom1  23934  flimopn  23983  hausflim  23989  flimcf  23990  flimclslem  23992  flimsncls  23994  cnpflf2  24008  cnpflf  24009  fclsneii  24025  fclsfnflim  24035  fcfnei  24043  flfcntr  24051  alexsubALTlem3  24057  alexsubALTlem4  24058  ptcmplem2  24061  cldsubg  24119  snclseqg  24124  qustgphaus  24131  tsmsgsum  24147  tsmsid  24148  tgptsmscld  24159  tsmsxplem1  24161  tsmsxplem2  24162  ust0  24228  ustuqtop1  24250  neipcfilu  24305  prdsdsf  24377  prdsxmetlem  24378  prdsmet  24380  imasdsf1olem  24383  xpsdsval  24391  prdsbl  24504  prdsxmslem2  24542  idnghm  24764  icccmplem2  24845  metnrmlem2  24882  ioombl  25600  volivth  25642  itg11  25726  i1fmulclem  25737  itg2mulclem  25781  itgsplitioo  25873  limcvallem  25906  limcdif  25911  ellimc2  25912  limcflf  25916  limcmpt2  25919  limcres  25921  cnplimc  25922  limccnp  25926  limccnp2  25927  limcco  25928  dvreslem  25944  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvcmulf  25982  dvef  26018  dvivth  26049  lhop2  26054  lhop  26055  ply1remlem  26204  fta1blem  26210  ig1peu  26214  ig1pdvds  26219  plyco0  26231  elply2  26235  plyf  26237  elplyr  26240  elplyd  26241  ply1term  26243  ply0  26247  plyeq0lem  26249  plyeq0  26250  plypf1  26251  plyaddlem  26254  plymullem  26255  dgrlem  26268  coef2  26270  coeidlem  26276  plyco  26280  coemulhi  26293  plycj  26317  plycjOLD  26319  vieta1  26354  taylf  26402  radcnv0  26459  abelth  26485  rlimcnp  27008  xrlimcnp  27011  amgm  27034  wilthlem2  27112  basellem7  27130  basellem9  27132  ppiprm  27194  chtprm  27196  musumsum  27235  muinv  27236  logexprlim  27269  perfectlem2  27274  dchrhash  27315  rpvmasum2  27556  ssltsn  27837  slerec  27864  cofcutr  27958  cutlt  27966  cutmax  27968  cutmin  27969  addsuniflem  28034  negsunif  28087  ssltmul1  28173  ssltmul2  28174  precsexlem11  28241  nohalf  28407  0reno  28429  axlowdimlem7  28963  axlowdimlem10  28966  upgrex  29109  upgr1elem  29129  uvtxnm1nbgr  29421  umgr2v2e  29543  cyclnumvtx  29820  0oo  30808  sh0le  31459  disjiunel  32609  preimane  32680  fnpreimac  32681  fsuppinisegfi  32696  fprodeq02  32825  s1f1  32927  gsumzresunsn  33059  gsumhashmul  33064  pmtrcnelor  33111  primefldgen1  33323  dvdsrspss  33415  elgrplsmsn  33418  lsmsnorb  33419  grplsm0l  33431  grplsmid  33432  0ringidl  33449  unitpidl1  33452  elrspunsn  33457  drngidl  33461  isprmidlc  33475  qsidomlem2  33481  ssdifidlprm  33486  mxidlprm  33498  mxidlirredi  33499  mxidlirred  33500  drngmxidl  33505  drngmxidlr  33506  qsdrngilem  33522  rsprprmprmidl  33550  rprmirredb  33560  1arithufdlem4  33575  lsatdim  33668  drngdimgt0  33669  dimkerim  33678  evls1fldgencl  33720  algextdeglem1  33758  algextdeglem2  33759  algextdeglem3  33760  algextdeglem4  33761  algextdeglem5  33762  rtelextdg2  33768  constrextdg2lem  33789  qtopt1  33834  locfinref  33840  zarcls0  33867  zarmxt1  33879  zarcmplem  33880  ordtrestNEW  33920  esumsnf  34065  esum2dlem  34093  rossros  34181  oms0  34299  carsggect  34320  eulerpartlems  34362  eulerpartlemgc  34364  eulerpartlemgh  34380  eulerpartlemgs2  34382  plymulx0  34562  circlemeth  34655  hgt750lemb  34671  hgt750leme  34673  bnj1452  35066  pthhashvtx  35133  subfacp1lem1  35184  subfacp1lem5  35189  erdszelem4  35199  erdszelem8  35203  sconnpi1  35244  cvmscld  35278  cvmlift2lem6  35313  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift2lem12  35319  mrsubvrs  35527  ellcsrspsn  35646  neibastop2lem  36361  topjoin  36366  fnejoin2  36370  weiunse  36469  pibt2  37418  lindsadd  37620  poimirlem3  37630  poimirlem9  37636  poimirlem28  37655  poimirlem32  37659  prdsbnd  37800  heiborlem8  37825  rrnequiv  37842  grpokerinj  37900  0idl  38032  prnc  38074  isfldidl  38075  lshpnel2N  38986  lsatfixedN  39010  lfl0f  39070  lkrlsp3  39105  elpaddatriN  39805  elpaddat  39806  elpadd2at  39808  pmodlem1  39848  osumcllem1N  39958  osumcllem2N  39959  osumcllem9N  39966  osumcllem10N  39967  pexmidlem6N  39977  pexmidlem7N  39978  dibss  41171  dochocsn  41383  dochsncom  41384  dochnel  41395  dihprrnlem1N  41426  dihprrnlem2  41427  djhlsmat  41429  dihsmsprn  41432  dvh4dimlem  41445  dvhdimlem  41446  dochsnnz  41452  dochsatshp  41453  dochsnshp  41455  dochexmid  41470  dochsnkr  41474  dochsnkr2cl  41476  dochfl1  41478  lcfl7lem  41501  lcfl6  41502  lcfl8  41504  lcfl9a  41507  lclkrlem2a  41509  lclkrlem2c  41511  lclkrlem2d  41512  lclkrlem2e  41513  lclkrlem2j  41518  lclkrlem2o  41523  lclkrlem2p  41524  lclkrlem2s  41527  lclkrlem2v  41530  lcfrlem14  41558  lcfrlem18  41562  lcfrlem19  41563  lcfrlem20  41564  lcfrlem23  41567  lcfrlem25  41569  lcdlkreqN  41624  mapdval4N  41634  mapdsn  41643  mapdhvmap  41771  hdmaprnlem4tN  41854  hdmapinvlem1  41920  hdmapinvlem2  41921  hdmapinvlem3  41922  hdmapinvlem4  41923  hdmapglem5  41924  hgmapvvlem3  41927  hdmapglem7a  41929  hdmapglem7b  41930  hdmapglem7  41931  hdmapoc  41933  aks6d1c5lem3  42138  deg1gprod  42141  sticksstones9  42155  sticksstones11  42157  rhmqusspan  42186  evlsbagval  42576  selvvvval  42595  0prjspnrel  42637  elrfi  42705  cmpfiiin  42708  mzpcompact2lem  42762  dfac11  43074  pwssplit4  43101  rngunsnply  43181  flcidc  43182  proot1mul  43206  iocinico  43224  cantnfresb  43337  iunrelexp0  43715  frege81d  43760  k0004lem3  44162  mnuunid  44296  binomcxplemnn0  44368  islptre  45634  limciccioolb  45636  limcicciooub  45652  limcresiooub  45657  limcresioolb  45658  ioccncflimc  45900  icccncfext  45902  icocncflimc  45904  cncfiooicc  45909  dvnprodlem2  45962  dirkercncflem2  46119  dirkercncflem3  46120  fourierdlem48  46169  fourierdlem49  46170  fourierdlem79  46200  fourierdlem101  46222  sge0sup  46406  hoidmvlelem2  46611  hoiqssbl  46640  hspmbllem1  46641  hspmbllem2  46642  ovnovollem1  46671  fsumsplitsndif  47360  imaelsetpreimafv  47382  perfectALTVlem2  47709  stgrclnbgr0  47932  isubgr3stgrlem3  47935  1hegrlfgr  48048  gsumdifsndf  48097  sepfsepc  48825