Theorem snssd 4789

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

Syntax hints:   → wi 4   ∈ wcel 2107   ⊆ wss 3931  {csn 4606

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-ss 3948  df-sn 4607

This theorem is referenced by:  intidg  5442  sofld  6187  fsnex  7285  fr3nr  7774  resf1extb  7938  resf1ext2b  7939  frrlem13  8305  wfrlem15OLD  8345  oeeui  8622  naddunif  8713  naddasslem1  8714  naddasslem2  8715  ecinxp  8814  ralxpmap  8918  xpdom3  9092  domunsn  9149  mapdom3  9171  isinf  9278  isinfOLD  9279  ac6sfi  9302  pwfilem  9338  finsschain  9381  ssfii  9441  marypha1lem  9455  unxpwdom2  9610  en2other2  10031  fseqenlem1  10046  axdc3lem4  10475  axdc4lem  10477  ttukeylem7  10537  fpwwe2lem12  10664  canthwe  10673  canthp1lem1  10674  wuncval2  10769  un0addcl  12542  un0mulcl  12543  ssfzunsnext  13591  fseq1p1m1  13620  hashbclem  14474  hashf1lem1  14477  fsumsplit1  15764  fsumge1  15816  incexclem  15855  isumltss  15867  fprodsplit1f  16009  rpnnen2lem11  16243  bitsinv1  16462  lcmfunsnlem2  16660  lcmfass  16666  phicl2  16788  vdwlem1  17002  vdwlem8  17009  vdwlem12  17013  vdwlem13  17014  0ram  17041  ramub1lem1  17047  ramub1lem2  17048  ramcl  17050  imasaddfnlem  17545  imasaddflem  17547  imasvscafn  17554  imasvscaf  17556  mrieqvlemd  17644  mreexmrid  17658  mreexexlem4d  17662  acsfiindd  18568  acsmapd  18569  gsumress  18665  0subm  18800  gsumvallem2  18817  0subgOLD  19140  trivsubgd  19141  trivsubgsnd  19142  trivnsgd  19160  cycsubg2cl  19199  kerf1ghm  19235  pmtrprfv  19440  odf1o1  19559  gex1  19578  sylow2alem1  19604  sylow2alem2  19605  lsm01  19658  lsm02  19659  lsmdisj  19668  lsmdisj2  19669  prmcyg  19881  gsumzadd  19909  gsumconst  19921  gsumdifsnd  19948  gsumpt  19949  gsumxp  19963  dmdprdd  19988  dprdfadd  20009  dprdres  20017  dprdz  20019  dprdsn  20025  dprddisj2  20028  dprd2da  20031  dprd2d2  20033  dmdprdsplit2lem  20034  dpjcntz  20041  dpjdisj  20042  dpjlsm  20043  dpjidcl  20047  ablfacrp  20055  ablfac1eu  20062  pgpfac1lem1  20063  pgpfac1lem3a  20065  pgpfac1lem3  20066  pgpfac1lem5  20068  pgpfaclem2  20071  acsfn1p  20769  lsssn0  20915  lss0ss  20916  lsptpcl  20946  lspsnvsi  20971  lspun0  20978  pwssplit1  21027  lsmpr  21057  lsppr  21061  lspsntri  21065  lspsolvlem  21113  lspsolv  21114  lsppratlem1  21118  lsppratlem3  21120  lsppratlem4  21121  islbs3  21126  lbsextlem4  21132  rnglidl0  21202  rsp1  21210  lidlnz  21215  lidldvgen  21307  mulgrhm2  21452  zndvds  21523  psrlidm  21937  psrridm  21938  mplmonmul  22009  mdetdiaglem  22553  mdetrlin  22557  mdetrsca  22558  mdetrsca2  22559  mdetrlin2  22562  mdetunilem5  22571  mdetunilem9  22575  mdetmul  22578  en2top  22940  rest0  23124  ordtrest  23157  iscnp4  23218  cnconst2  23238  cnpdis  23248  ist1-2  23302  cnt1  23305  dishaus  23337  discmp  23353  cmpcld  23357  conncompid  23386  dis2ndc  23415  dislly  23452  dissnref  23483  comppfsc  23487  llycmpkgen2  23505  cmpkgen  23506  1stckgenlem  23508  1stckgen  23509  ptbasfi  23536  txdis  23587  txdis1cn  23590  txcmplem1  23596  xkohaus  23608  xkoptsub  23609  xkoinjcn  23642  snfbas  23821  trnei  23847  isufil2  23863  ufileu  23874  filufint  23875  uffixsn  23880  ufildom1  23881  flimopn  23930  hausflim  23936  flimcf  23937  flimclslem  23939  flimsncls  23941  cnpflf2  23955  cnpflf  23956  fclsneii  23972  fclsfnflim  23982  fcfnei  23990  flfcntr  23998  alexsubALTlem3  24004  alexsubALTlem4  24005  ptcmplem2  24008  cldsubg  24066  snclseqg  24071  qustgphaus  24078  tsmsgsum  24094  tsmsid  24095  tgptsmscld  24106  tsmsxplem1  24108  tsmsxplem2  24109  ust0  24175  ustuqtop1  24197  neipcfilu  24251  prdsdsf  24323  prdsxmetlem  24324  prdsmet  24326  imasdsf1olem  24329  xpsdsval  24337  prdsbl  24449  prdsxmslem2  24487  idnghm  24701  icccmplem2  24782  metnrmlem2  24819  ioombl  25537  volivth  25579  itg11  25663  i1fmulclem  25674  itg2mulclem  25718  itgsplitioo  25810  limcvallem  25843  limcdif  25848  ellimc2  25849  limcflf  25853  limcmpt2  25856  limcres  25858  cnplimc  25859  limccnp  25863  limccnp2  25864  limcco  25865  dvreslem  25881  dvaddbr  25911  dvmulbr  25912  dvmulbrOLD  25913  dvcmulf  25919  dvef  25955  dvivth  25986  lhop2  25991  lhop  25992  ply1remlem  26141  fta1blem  26147  ig1peu  26151  ig1pdvds  26156  plyco0  26168  elply2  26172  plyf  26174  elplyr  26177  elplyd  26178  ply1term  26180  ply0  26184  plyeq0lem  26186  plyeq0  26187  plypf1  26188  plyaddlem  26191  plymullem  26192  dgrlem  26205  coef2  26207  coeidlem  26213  plyco  26217  coemulhi  26230  plycj  26254  plycjOLD  26256  vieta1  26291  taylf  26339  radcnv0  26396  abelth  26422  rlimcnp  26945  xrlimcnp  26948  amgm  26971  wilthlem2  27049  basellem7  27067  basellem9  27069  ppiprm  27131  chtprm  27133  musumsum  27172  muinv  27173  logexprlim  27206  perfectlem2  27211  dchrhash  27252  rpvmasum2  27493  ssltsn  27774  slerec  27801  cofcutr  27895  cutlt  27903  cutmax  27905  cutmin  27906  addsuniflem  27971  negsunif  28024  ssltmul1  28110  ssltmul2  28111  precsexlem11  28178  nohalf  28344  0reno  28366  axlowdimlem7  28894  axlowdimlem10  28897  upgrex  29038  upgr1elem  29058  uvtxnm1nbgr  29350  umgr2v2e  29472  cyclnumvtx  29749  0oo  30737  sh0le  31388  disjiunel  32545  preimane  32616  fnpreimac  32617  fsuppinisegfi  32632  fprodeq02  32770  s1f1  32872  gsumzresunsn  33003  gsumhashmul  33008  pmtrcnelor  33055  primefldgen1  33268  dvdsrspss  33355  elgrplsmsn  33358  lsmsnorb  33359  grplsm0l  33371  grplsmid  33372  0ringidl  33389  unitpidl1  33392  elrspunsn  33397  drngidl  33401  isprmidlc  33415  qsidomlem2  33421  ssdifidlprm  33426  mxidlprm  33438  mxidlirredi  33439  mxidlirred  33440  drngmxidl  33445  drngmxidlr  33446  qsdrngilem  33462  rsprprmprmidl  33490  rprmirredb  33500  1arithufdlem4  33515  lsatdim  33608  drngdimgt0  33609  dimkerim  33618  evls1fldgencl  33662  algextdeglem1  33702  algextdeglem2  33703  algextdeglem3  33704  algextdeglem4  33705  algextdeglem5  33706  rtelextdg2  33712  constrextdg2lem  33733  constrext2chnlem  33735  constrfiss  33736  qtopt1  33809  locfinref  33815  zarcls0  33842  zarmxt1  33854  zarcmplem  33855  ordtrestNEW  33895  esumsnf  34040  esum2dlem  34068  rossros  34156  oms0  34274  carsggect  34295  eulerpartlems  34337  eulerpartlemgc  34339  eulerpartlemgh  34355  eulerpartlemgs2  34357  plymulx0  34537  circlemeth  34630  hgt750lemb  34646  hgt750leme  34648  bnj1452  35041  pthhashvtx  35108  subfacp1lem1  35159  subfacp1lem5  35164  erdszelem4  35174  erdszelem8  35178  sconnpi1  35219  cvmscld  35253  cvmlift2lem6  35288  cvmlift2lem9  35291  cvmlift2lem11  35293  cvmlift2lem12  35294  mrsubvrs  35502  ellcsrspsn  35621  neibastop2lem  36336  topjoin  36341  fnejoin2  36345  weiunse  36444  pibt2  37393  lindsadd  37595  poimirlem3  37605  poimirlem9  37611  poimirlem28  37630  poimirlem32  37634  prdsbnd  37775  heiborlem8  37800  rrnequiv  37817  grpokerinj  37875  0idl  38007  prnc  38049  isfldidl  38050  lshpnel2N  38961  lsatfixedN  38985  lfl0f  39045  lkrlsp3  39080  elpaddatriN  39780  elpaddat  39781  elpadd2at  39783  pmodlem1  39823  osumcllem1N  39933  osumcllem2N  39934  osumcllem9N  39941  osumcllem10N  39942  pexmidlem6N  39952  pexmidlem7N  39953  dibss  41146  dochocsn  41358  dochsncom  41359  dochnel  41370  dihprrnlem1N  41401  dihprrnlem2  41402  djhlsmat  41404  dihsmsprn  41407  dvh4dimlem  41420  dvhdimlem  41421  dochsnnz  41427  dochsatshp  41428  dochsnshp  41430  dochexmid  41445  dochsnkr  41449  dochsnkr2cl  41451  dochfl1  41453  lcfl7lem  41476  lcfl6  41477  lcfl8  41479  lcfl9a  41482  lclkrlem2a  41484  lclkrlem2c  41486  lclkrlem2d  41487  lclkrlem2e  41488  lclkrlem2j  41493  lclkrlem2o  41498  lclkrlem2p  41499  lclkrlem2s  41502  lclkrlem2v  41505  lcfrlem14  41533  lcfrlem18  41537  lcfrlem19  41538  lcfrlem20  41539  lcfrlem23  41542  lcfrlem25  41544  lcdlkreqN  41599  mapdval4N  41609  mapdsn  41618  mapdhvmap  41746  hdmaprnlem4tN  41829  hdmapinvlem1  41895  hdmapinvlem2  41896  hdmapinvlem3  41897  hdmapinvlem4  41898  hdmapglem5  41899  hgmapvvlem3  41902  hdmapglem7a  41904  hdmapglem7b  41905  hdmapglem7  41906  hdmapoc  41908  aks6d1c5lem3  42113  deg1gprod  42116  sticksstones9  42130  sticksstones11  42132  rhmqusspan  42161  evlsbagval  42555  selvvvval  42574  0prjspnrel  42616  elrfi  42683  cmpfiiin  42686  mzpcompact2lem  42740  dfac11  43052  pwssplit4  43079  rngunsnply  43159  flcidc  43160  proot1mul  43184  iocinico  43202  cantnfresb  43314  iunrelexp0  43692  frege81d  43737  k0004lem3  44139  mnuunid  44268  binomcxplemnn0  44340  islptre  45606  limciccioolb  45608  limcicciooub  45624  limcresiooub  45629  limcresioolb  45630  ioccncflimc  45872  icccncfext  45874  icocncflimc  45876  cncfiooicc  45881  dvnprodlem2  45934  dirkercncflem2  46091  dirkercncflem3  46092  fourierdlem48  46141  fourierdlem49  46142  fourierdlem79  46172  fourierdlem101  46194  sge0sup  46378  hoidmvlelem2  46583  hoiqssbl  46612  hspmbllem1  46613  hspmbllem2  46614  ovnovollem1  46643  fsumsplitsndif  47333  imaelsetpreimafv  47355  perfectALTVlem2  47682  stgrclnbgr0  47905  isubgr3stgrlem3  47908  1hegrlfgr  48021  gsumdifsndf  48070  sepfsepc  48809