Theorem snssd 4730

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3889  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-ss 3906  df-sn 4568

This theorem is referenced by:  intidg  5409  sofld  6151  fsnex  7238  fr3nr  7726  resf1extb  7885  resf1ext2b  7886  frrlem13  8248  oeeui  8538  naddunif  8629  naddasslem1  8630  naddasslem2  8631  ecinxp  8739  ralxpmap  8844  xpdom3  9013  domunsn  9065  mapdom3  9087  isinf  9175  ac6sfi  9194  pwfilem  9228  finsschain  9269  ssfii  9332  marypha1lem  9346  unxpwdom2  9503  en2other2  9931  fseqenlem1  9946  axdc3lem4  10375  axdc4lem  10377  ttukeylem7  10437  fpwwe2lem12  10565  canthwe  10574  canthp1lem1  10575  wuncval2  10670  un0addcl  12470  un0mulcl  12471  ssfzunsnext  13523  fseq1p1m1  13552  hashbclem  14414  hashf1lem1  14417  fsumsplit1  15707  fsumge1  15760  incexclem  15801  isumltss  15813  fprodsplit1f  15955  rpnnen2lem11  16191  bitsinv1  16411  lcmfunsnlem2  16609  lcmfass  16615  phicl2  16738  vdwlem1  16952  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  0ram  16991  ramub1lem1  16997  ramub1lem2  16998  ramcl  17000  imasaddfnlem  17492  imasaddflem  17494  imasvscafn  17501  imasvscaf  17503  mrieqvlemd  17595  mreexmrid  17609  mreexexlem4d  17613  acsfiindd  18519  acsmapd  18520  chnccat  18592  gsumress  18650  0subm  18785  gsumvallem2  18802  trivsubgd  19128  trivsubgsnd  19129  trivnsgd  19147  cycsubg2cl  19186  kerf1ghm  19222  pmtrprfv  19428  odf1o1  19547  gex1  19566  sylow2alem1  19592  sylow2alem2  19593  lsm01  19646  lsm02  19647  lsmdisj  19656  lsmdisj2  19657  prmcyg  19869  gsumzadd  19897  gsumconst  19909  gsumdifsnd  19936  gsumpt  19937  gsumxp  19951  dmdprdd  19976  dprdfadd  19997  dprdres  20005  dprdz  20007  dprdsn  20013  dprddisj2  20016  dprd2da  20019  dprd2d2  20021  dmdprdsplit2lem  20022  dpjcntz  20029  dpjdisj  20030  dpjlsm  20031  dpjidcl  20035  ablfacrp  20043  ablfac1eu  20050  pgpfac1lem1  20051  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem5  20056  pgpfaclem2  20059  acsfn1p  20776  lsssn0  20943  lss0ss  20944  lsptpcl  20974  lspsnvsi  20999  lspun0  21006  pwssplit1  21054  lsmpr  21084  lsppr  21088  lspsntri  21092  lspsolvlem  21140  lspsolv  21141  lsppratlem1  21145  lsppratlem3  21147  lsppratlem4  21148  islbs3  21153  lbsextlem4  21159  rnglidl0  21227  rsp1  21235  lidlnz  21240  lidldvgen  21332  mulgrhm2  21458  zndvds  21529  psrlidm  21940  psrridm  21941  mplmonmul  22014  mdetdiaglem  22563  mdetrlin  22567  mdetrsca  22568  mdetrsca2  22569  mdetrlin2  22572  mdetunilem5  22581  mdetunilem9  22585  mdetmul  22588  en2top  22950  rest0  23134  ordtrest  23167  iscnp4  23228  cnconst2  23248  cnpdis  23258  ist1-2  23312  cnt1  23315  dishaus  23347  discmp  23363  cmpcld  23367  conncompid  23396  dis2ndc  23425  dislly  23462  dissnref  23493  comppfsc  23497  llycmpkgen2  23515  cmpkgen  23516  1stckgenlem  23518  1stckgen  23519  ptbasfi  23546  txdis  23597  txdis1cn  23600  txcmplem1  23606  xkohaus  23618  xkoptsub  23619  xkoinjcn  23652  snfbas  23831  trnei  23857  isufil2  23873  ufileu  23884  filufint  23885  uffixsn  23890  ufildom1  23891  flimopn  23940  hausflim  23946  flimcf  23947  flimclslem  23949  flimsncls  23951  cnpflf2  23965  cnpflf  23966  fclsneii  23982  fclsfnflim  23992  fcfnei  24000  flfcntr  24008  alexsubALTlem3  24014  alexsubALTlem4  24015  ptcmplem2  24018  cldsubg  24076  snclseqg  24081  qustgphaus  24088  tsmsgsum  24104  tsmsid  24105  tgptsmscld  24116  tsmsxplem1  24118  tsmsxplem2  24119  ust0  24185  ustuqtop1  24206  neipcfilu  24260  prdsdsf  24332  prdsxmetlem  24333  prdsmet  24335  imasdsf1olem  24338  xpsdsval  24346  prdsbl  24456  prdsxmslem2  24494  idnghm  24708  icccmplem2  24789  metnrmlem2  24826  ioombl  25532  volivth  25574  itg11  25658  i1fmulclem  25669  itg2mulclem  25713  itgsplitioo  25805  limcvallem  25838  limcdif  25843  ellimc2  25844  limcflf  25848  limcmpt2  25851  limcres  25853  cnplimc  25854  limccnp  25858  limccnp2  25859  limcco  25860  dvreslem  25876  dvaddbr  25905  dvmulbr  25906  dvcmulf  25912  dvef  25947  dvivth  25977  lhop2  25982  lhop  25983  ply1remlem  26130  fta1blem  26136  ig1peu  26140  ig1pdvds  26145  plyco0  26157  elply2  26161  plyf  26163  elplyr  26166  elplyd  26167  ply1term  26169  ply0  26173  plyeq0lem  26175  plyeq0  26176  plypf1  26177  plyaddlem  26180  plymullem  26181  dgrlem  26194  coef2  26196  coeidlem  26202  plyco  26206  coemulhi  26219  plycj  26242  plycjOLD  26244  vieta1  26278  taylf  26326  radcnv0  26381  abelth  26406  rlimcnp  26929  xrlimcnp  26932  amgm  26954  wilthlem2  27032  basellem7  27050  basellem9  27052  ppiprm  27114  chtprm  27116  musumsum  27155  muinv  27156  logexprlim  27188  perfectlem2  27193  dchrhash  27234  rpvmasum2  27475  sltssnb  27761  conway  27771  lesrec  27791  eqcuts3  27796  cofcutr  27916  cutlt  27924  cutmax  27926  cutmin  27927  cutminmax  27928  addsuniflem  27993  negsunif  28047  sltmuls1  28139  sltmuls2  28140  precsexlem11  28209  oncutlt  28256  n0fincut  28347  bdaypw2n0bndlem  28455  axlowdimlem7  29017  axlowdimlem10  29020  upgrex  29161  upgr1elem  29181  uvtxnm1nbgr  29473  umgr2v2e  29594  cyclnumvtx  29868  0oo  30860  sh0le  31511  disjiunel  32666  preimane  32742  fnpreimac  32743  fsuppinisegfi  32760  fprodeq02  32897  indsn  32923  s1f1  33003  gsumzresunsn  33123  gsumhashmul  33128  pmtrcnelor  33152  primefldgen1  33382  dvdsrspss  33447  elgrplsmsn  33450  lsmsnorb  33451  grplsm0l  33463  grplsmid  33464  0ringidl  33481  unitpidl1  33484  elrspunsn  33489  drngidl  33493  isprmidlc  33507  qsidomlem2  33513  ssdifidlprm  33518  mxidlprm  33530  mxidlirredi  33531  mxidlirred  33532  drngmxidl  33537  drngmxidlr  33538  qsdrngilem  33554  rsprprmprmidl  33582  rprmirredb  33592  1arithufdlem4  33607  mvrvalind  33682  mplmulmvr  33683  evlextv  33686  psrmonmul  33694  esplyfval0  33708  esplyfvaln  33718  esplyind  33719  esplyindfv  33720  vietalem  33723  lsatdim  33761  drngdimgt0  33762  dimkerim  33771  evls1fldgencl  33814  algextdeglem1  33861  algextdeglem2  33862  algextdeglem3  33863  algextdeglem4  33864  algextdeglem5  33865  rtelextdg2  33871  constrextdg2lem  33892  constrext2chnlem  33894  constrfiss  33895  qtopt1  33979  locfinref  33985  zarcls0  34012  zarmxt1  34024  zarcmplem  34025  ordtrestNEW  34065  esumsnf  34208  esum2dlem  34236  rossros  34324  oms0  34441  carsggect  34462  eulerpartlems  34504  eulerpartlemgc  34506  eulerpartlemgh  34522  eulerpartlemgs2  34524  plymulx0  34691  circlemeth  34784  hgt750lemb  34800  hgt750leme  34802  bnj1452  35194  pthhashvtx  35310  subfacp1lem1  35361  subfacp1lem5  35366  erdszelem4  35376  erdszelem8  35380  sconnpi1  35421  cvmscld  35455  cvmlift2lem6  35490  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift2lem12  35496  mrsubvrs  35704  ellcsrspsn  35823  neibastop2lem  36542  topjoin  36547  fnejoin2  36551  weiunse  36650  pibt2  37733  lindsadd  37934  poimirlem3  37944  poimirlem9  37950  poimirlem28  37969  poimirlem32  37973  prdsbnd  38114  heiborlem8  38139  rrnequiv  38156  grpokerinj  38214  0idl  38346  prnc  38388  isfldidl  38389  lshpnel2N  39431  lsatfixedN  39455  lfl0f  39515  lkrlsp3  39550  elpaddatriN  40249  elpaddat  40250  elpadd2at  40252  pmodlem1  40292  osumcllem1N  40402  osumcllem2N  40403  osumcllem9N  40410  osumcllem10N  40411  pexmidlem6N  40421  pexmidlem7N  40422  dibss  41615  dochocsn  41827  dochsncom  41828  dochnel  41839  dihprrnlem1N  41870  dihprrnlem2  41871  djhlsmat  41873  dihsmsprn  41876  dvh4dimlem  41889  dvhdimlem  41890  dochsnnz  41896  dochsatshp  41897  dochsnshp  41899  dochexmid  41914  dochsnkr  41918  dochsnkr2cl  41920  dochfl1  41922  lcfl7lem  41945  lcfl6  41946  lcfl8  41948  lcfl9a  41951  lclkrlem2a  41953  lclkrlem2c  41955  lclkrlem2d  41956  lclkrlem2e  41957  lclkrlem2j  41962  lclkrlem2o  41967  lclkrlem2p  41968  lclkrlem2s  41971  lclkrlem2v  41974  lcfrlem14  42002  lcfrlem18  42006  lcfrlem19  42007  lcfrlem20  42008  lcfrlem23  42011  lcfrlem25  42013  lcdlkreqN  42068  mapdval4N  42078  mapdsn  42087  mapdhvmap  42215  hdmaprnlem4tN  42298  hdmapinvlem1  42364  hdmapinvlem2  42365  hdmapinvlem3  42366  hdmapinvlem4  42367  hdmapglem5  42368  hgmapvvlem3  42371  hdmapglem7a  42373  hdmapglem7b  42374  hdmapglem7  42375  hdmapoc  42377  aks6d1c5lem3  42576  deg1gprod  42579  sticksstones9  42593  sticksstones11  42595  rhmqusspan  42624  evlsbagval  43002  selvvvval  43018  0prjspnrel  43060  elrfi  43126  cmpfiiin  43129  mzpcompact2lem  43183  dfac11  43490  pwssplit4  43517  rngunsnply  43597  flcidc  43598  proot1mul  43622  iocinico  43640  cantnfresb  43752  iunrelexp0  44129  frege81d  44174  k0004lem3  44576  mnuunid  44704  binomcxplemnn0  44776  islptre  46049  limciccioolb  46051  limcicciooub  46065  limcresiooub  46070  limcresioolb  46071  ioccncflimc  46313  icccncfext  46315  icocncflimc  46317  cncfiooicc  46322  dvnprodlem2  46375  dirkercncflem2  46532  dirkercncflem3  46533  fourierdlem48  46582  fourierdlem49  46583  fourierdlem79  46613  fourierdlem101  46635  sge0sup  46819  hoidmvlelem2  47024  hoiqssbl  47053  hspmbllem1  47054  hspmbllem2  47055  ovnovollem1  47084  fsumsplitsndif  47829  imaelsetpreimafv  47855  perfectALTVlem2  48198  stgrclnbgr0  48441  isubgr3stgrlem3  48444  1hegrlfgr  48608  gsumdifsndf  48657  sepfsepc  49403  discsubc  49539  iinfconstbas  49541