Theorem snssd 4745

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

Syntax hints:   → wi 4   ∈ wcel 2142   ⊆ wss 3904  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-ss 3921  df-sn 4583

This theorem is referenced by:  intidg  5424  sofld  6173  fsnex  7267  fr3nr  7755  resf1extb  7915  resf1ext2b  7916  frrlem13  8279  oeeui  8572  naddunif  8664  naddasslem1  8665  naddasslem2  8666  ecinxp  8774  ralxpmap  8878  xpdom3  9047  domunsn  9099  mapdom3  9121  isinf  9209  ac6sfi  9228  pwfilem  9262  finsschain  9302  ssfii  9365  marypha1lem  9379  unxpwdom2  9536  en2other2  9965  fseqenlem1  9980  axdc3lem4  10410  axdc4lem  10412  ttukeylem7  10472  fpwwe2lem12  10600  canthwe  10609  canthp1lem1  10610  wuncval2  10705  un0addcl  12514  un0mulcl  12515  ssfzunsnext  13574  fseq1p1m1  13603  hashbclem  14465  hashf1lem1  14468  fsumsplit1  15772  fsumge1  15825  incexclem  15866  isumltss  15878  fprodsplit1f  16020  rpnnen2lem11  16256  bitsinv1  16476  lcmfunsnlem2  16674  lcmfass  16680  phicl2  16803  vdwlem1  17017  vdwlem8  17024  vdwlem12  17028  vdwlem13  17029  0ram  17056  ramub1lem1  17062  ramub1lem2  17063  ramcl  17065  imasaddfnlem  17558  imasaddflem  17560  imasvscafn  17567  imasvscaf  17569  mrieqvlemd  17661  mreexmrid  17675  mreexexlem4d  17679  acsfiindd  18585  acsmapd  18586  chnccat  18658  gsumress  18716  0subm  18851  gsumvallem2  18868  trivsubgd  19194  trivsubgsnd  19195  trivnsgd  19213  cycsubg2cl  19252  kerf1ghm  19287  pmtrprfv  19493  odf1o1  19612  gex1  19631  sylow2alem1  19657  sylow2alem2  19658  lsm01  19711  lsm02  19712  lsmdisj  19721  lsmdisj2  19722  prmcyg  19934  gsumzadd  19962  gsumconst  19974  gsumdifsnd  20001  gsumpt  20002  gsumxp  20016  dmdprdd  20041  dprdfadd  20062  dprdres  20070  dprdz  20072  dprdsn  20078  dprddisj2  20081  dprd2da  20084  dprd2d2  20086  dmdprdsplit2lem  20087  dpjcntz  20094  dpjdisj  20095  dpjlsm  20096  dpjidcl  20100  ablfacrp  20108  ablfac1eu  20115  pgpfac1lem1  20116  pgpfac1lem3a  20118  pgpfac1lem3  20119  pgpfac1lem5  20121  pgpfaclem2  20124  acsfn1p  20848  lsssn0  21015  lss0ss  21016  lsptpcl  21046  lspsnvsi  21071  lspun0  21078  pwssplit1  21126  lsmpr  21156  lsppr  21160  lspsntri  21164  lspsolvlem  21212  lspsolv  21213  lsppratlem1  21217  lsppratlem3  21219  lsppratlem4  21220  islbs3  21225  lbsextlem4  21231  rnglidl0  21299  rsp1  21307  lidlnz  21312  lidldvgen  21404  mulgrhm2  21530  zndvds  21601  psrlidm  22013  psrridm  22014  mplmonmul  22089  selvvvval  22195  mdetdiaglem  22658  mdetrlin  22662  mdetrsca  22663  mdetrsca2  22664  mdetrlin2  22667  mdetunilem5  22676  mdetunilem9  22680  mdetmul  22683  en2top  23045  rest0  23229  ordtrest  23262  iscnp4  23323  cnconst2  23343  cnpdis  23353  ist1-2  23407  cnt1  23410  dishaus  23442  discmp  23458  cmpcld  23462  conncompid  23491  dis2ndc  23520  dislly  23557  dissnref  23588  comppfsc  23592  llycmpkgen2  23610  cmpkgen  23611  1stckgenlem  23613  1stckgen  23614  ptbasfi  23641  txdis  23692  txdis1cn  23695  txcmplem1  23701  xkohaus  23713  xkoptsub  23714  xkoinjcn  23747  snfbas  23926  trnei  23952  isufil2  23968  ufileu  23979  filufint  23980  uffixsn  23985  ufildom1  23986  flimopn  24035  hausflim  24041  flimcf  24042  flimclslem  24044  flimsncls  24046  cnpflf2  24060  cnpflf  24061  fclsneii  24077  fclsfnflim  24087  fcfnei  24095  flfcntr  24103  alexsubALTlem3  24109  alexsubALTlem4  24110  ptcmplem2  24113  cldsubg  24171  snclseqg  24176  qustgphaus  24183  tsmsgsum  24199  tsmsid  24200  tgptsmscld  24211  tsmsxplem1  24213  tsmsxplem2  24214  ust0  24280  ustuqtop1  24301  neipcfilu  24355  prdsdsf  24427  prdsxmetlem  24428  prdsmet  24430  imasdsf1olem  24433  xpsdsval  24441  prdsbl  24551  prdsxmslem2  24589  idnghm  24803  icccmplem2  24884  metnrmlem2  24921  ioombl  25627  volivth  25669  itg11  25753  i1fmulclem  25764  itg2mulclem  25808  itgsplitioo  25900  limcvallem  25933  limcdif  25938  ellimc2  25939  limcflf  25943  limcmpt2  25946  limcres  25948  cnplimc  25949  limccnp  25953  limccnp2  25954  limcco  25955  dvreslem  25971  dvaddbr  26000  dvmulbr  26001  dvcmulf  26007  dvef  26042  dvivth  26072  lhop2  26077  lhop  26078  ply1remlem  26225  fta1blem  26231  ig1peu  26235  ig1pdvds  26240  plyco0  26252  elply2  26256  plyf  26258  elplyr  26261  elplyd  26262  ply1term  26264  ply0  26268  plyeq0lem  26270  plyeq0  26271  plypf1  26272  plyaddlem  26275  plymullem  26276  dgrlem  26289  coef2  26291  coeidlem  26297  plyco  26301  coemulhi  26314  plycj  26337  plycjOLD  26339  plyn0mulidp  26345  vieta1  26376  taylf  26424  radcnv0  26479  abelth  26504  rlimcnp  27030  xrlimcnp  27033  amgm  27055  wilthlem2  27133  basellem7  27151  basellem9  27153  ppiprm  27215  chtprm  27217  musumsum  27256  muinv  27257  logexprlim  27289  perfectlem2  27294  dchrhash  27335  rpvmasum2  27576  sltssnb  27862  conway  27872  lesrec  27892  eqcuts3  27897  cofcutr  28017  cutlt  28025  cutmax  28027  cutmin  28028  cutminmax  28029  addsuniflem  28094  negsunif  28148  sltmuls1  28240  sltmuls2  28241  precsexlem11  28310  oncutlt  28357  n0fincut  28448  bdaypw2n0bndlem  28556  axlowdimlem7  29149  axlowdimlem10  29152  upgrex  29293  upgr1elem  29313  uvtxnm1nbgr  29605  umgr2v2e  29726  cyclnumvtx  30000  0oo  30992  sh0le  31643  disjiunel  32796  preimane  32871  fnpreimac  32872  fsuppinisegfi  32889  fprodeq02  33026  indsn  33041  s1f1  33121  gsumzresunsn  33242  gsumhashmul  33247  pmtrcnelor  33271  primefldgen1  33508  dvdsrspss  33573  elgrplsmsn  33576  lsmsnorb  33577  grplsm0l  33589  grplsmid  33590  0ringidl  33607  unitpidl1  33610  elrspunsn  33615  drngidl  33619  isprmidlc  33633  qsidomlem2  33640  ssdifidlprm  33645  mxidlprm  33658  mxidlirredi  33659  mxidlirred  33660  drngmxidl  33665  drngmxidlr  33666  qsdrngilem  33682  dflringlem  33690  rsprprmprmidl  33718  rprmirredb  33728  1arithufdlem4  33743  selvply1rhmlem1  33817  selvply1rhmlem2  33818  selvply1rhmlem4  33820  selvply1rhmlem5  33821  selvply1rhm  33822  selvply1rhm0  33823  mvrvalind  33835  mplmulmvr  33836  evlextv  33839  psrmonmul  33847  esplyfval0  33861  esplyfvaln  33871  esplyind  33872  esplyindfv  33873  vietalem  33876  lsatdim  33914  drngdimgt0  33915  dimkerim  33924  evls1fldgencl  33967  algextdeglem1  34014  algextdeglem2  34015  algextdeglem3  34016  algextdeglem4  34017  algextdeglem5  34018  rtelextdg2  34024  constrextdg2lem  34045  constrext2chnlem  34047  constrfiss  34048  qtopt1  34132  locfinref  34138  zarcls0  34165  zarmxt1  34177  zarcmplem  34178  ordtrestNEW  34218  esumsnf  34361  esum2dlem  34389  rossros  34477  oms0  34594  carsggect  34615  eulerpartlems  34657  eulerpartlemgc  34659  eulerpartlemgh  34675  eulerpartlemgs2  34677  circlemeth  34934  hgt750lemb  34950  hgt750leme  34952  bnj1452  35347  pthhashvtx  35478  subfacp1lem1  35529  subfacp1lem5  35534  erdszelem4  35544  erdszelem8  35548  sconnpi1  35589  cvmscld  35623  cvmlift2lem6  35658  cvmlift2lem9  35661  cvmlift2lem11  35663  cvmlift2lem12  35664  mrsubvrs  35872  ellcsrspsn  35991  neibastop2lem  36720  topjoin  36725  fnejoin2  36729  weiunse  36828  pibt2  37911  lindsadd  38112  poimirlem3  38122  poimirlem9  38128  poimirlem28  38147  poimirlem32  38151  prdsbnd  38292  heiborlem8  38317  rrnequiv  38334  grpokerinj  38392  0idl  38524  prnc  38566  isfldidl  38567  lshpnel2N  39609  lsatfixedN  39633  lfl0f  39693  lkrlsp3  39728  elpaddatriN  40427  elpaddat  40428  elpadd2at  40430  pmodlem1  40470  osumcllem1N  40580  osumcllem2N  40581  osumcllem9N  40588  osumcllem10N  40589  pexmidlem6N  40599  pexmidlem7N  40600  dibss  41793  dochocsn  42005  dochsncom  42006  dochnel  42017  dihprrnlem1N  42048  dihprrnlem2  42049  djhlsmat  42051  dihsmsprn  42054  dvh4dimlem  42067  dvhdimlem  42068  dochsnnz  42074  dochsatshp  42075  dochsnshp  42077  dochexmid  42092  dochsnkr  42096  dochsnkr2cl  42098  dochfl1  42100  lcfl7lem  42123  lcfl6  42124  lcfl8  42126  lcfl9a  42129  lclkrlem2a  42131  lclkrlem2c  42133  lclkrlem2d  42134  lclkrlem2e  42135  lclkrlem2j  42140  lclkrlem2o  42145  lclkrlem2p  42146  lclkrlem2s  42149  lclkrlem2v  42152  lcfrlem14  42180  lcfrlem18  42184  lcfrlem19  42185  lcfrlem20  42186  lcfrlem23  42189  lcfrlem25  42191  lcdlkreqN  42246  mapdval4N  42256  mapdsn  42265  mapdhvmap  42393  hdmaprnlem4tN  42476  hdmapinvlem1  42542  hdmapinvlem2  42543  hdmapinvlem3  42544  hdmapinvlem4  42545  hdmapglem5  42546  hgmapvvlem3  42549  hdmapglem7a  42551  hdmapglem7b  42552  hdmapglem7  42553  hdmapoc  42555  aks6d1c5lem3  42754  deg1gprod  42757  sticksstones9  42771  sticksstones11  42773  rhmqusspan  42802  evlsbagval  43168  0prjspnrel  43209  elrfi  43275  cmpfiiin  43278  mzpcompact2lem  43332  dfac11  43639  pwssplit4  43666  rngunsnply  43746  flcidc  43747  proot1mul  43771  iocinico  43789  cantnfresb  43901  iunrelexp0  44278  frege81d  44323  k0004lem3  44725  mnuunid  44853  binomcxplemnn0  44925  islptre  46195  limciccioolb  46197  limcicciooub  46211  limcresiooub  46216  limcresioolb  46217  ioccncflimc  46459  icccncfext  46461  icocncflimc  46463  cncfiooicc  46468  dvnprodlem2  46521  dirkercncflem2  46678  dirkercncflem3  46679  fourierdlem48  46728  fourierdlem49  46729  fourierdlem79  46759  fourierdlem101  46781  sge0sup  46965  hoidmvlelem2  47170  hoiqssbl  47199  hspmbllem1  47200  hspmbllem2  47201  ovnovollem1  47230  fsumsplitsndif  47975  imaelsetpreimafv  48001  perfectALTVlem2  48344  stgrclnbgr0  48587  isubgr3stgrlem3  48590  1hegrlfgr  48754  gsumdifsndf  48803  sepfsepc  49549  discsubc  49685  iinfconstbas  49687