Theorem snssd 4769

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

Syntax hints:   → wi 4   ∈ wcel 2109   ⊆ wss 3911  {csn 4585

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-ss 3928  df-sn 4586

This theorem is referenced by:  intidg  5412  sofld  6148  fsnex  7240  fr3nr  7728  resf1extb  7890  resf1ext2b  7891  frrlem13  8254  oeeui  8543  naddunif  8634  naddasslem1  8635  naddasslem2  8636  ecinxp  8742  ralxpmap  8846  xpdom3  9016  domunsn  9068  mapdom3  9090  isinf  9183  isinfOLD  9184  ac6sfi  9207  pwfilem  9243  finsschain  9286  ssfii  9346  marypha1lem  9360  unxpwdom2  9517  en2other2  9938  fseqenlem1  9953  axdc3lem4  10382  axdc4lem  10384  ttukeylem7  10444  fpwwe2lem12  10571  canthwe  10580  canthp1lem1  10581  wuncval2  10676  un0addcl  12451  un0mulcl  12452  ssfzunsnext  13506  fseq1p1m1  13535  hashbclem  14393  hashf1lem1  14396  fsumsplit1  15687  fsumge1  15739  incexclem  15778  isumltss  15790  fprodsplit1f  15932  rpnnen2lem11  16168  bitsinv1  16388  lcmfunsnlem2  16586  lcmfass  16592  phicl2  16714  vdwlem1  16928  vdwlem8  16935  vdwlem12  16939  vdwlem13  16940  0ram  16967  ramub1lem1  16973  ramub1lem2  16974  ramcl  16976  imasaddfnlem  17467  imasaddflem  17469  imasvscafn  17476  imasvscaf  17478  mrieqvlemd  17570  mreexmrid  17584  mreexexlem4d  17588  acsfiindd  18494  acsmapd  18495  gsumress  18591  0subm  18726  gsumvallem2  18743  0subgOLD  19066  trivsubgd  19067  trivsubgsnd  19068  trivnsgd  19086  cycsubg2cl  19125  kerf1ghm  19161  pmtrprfv  19367  odf1o1  19486  gex1  19505  sylow2alem1  19531  sylow2alem2  19532  lsm01  19585  lsm02  19586  lsmdisj  19595  lsmdisj2  19596  prmcyg  19808  gsumzadd  19836  gsumconst  19848  gsumdifsnd  19875  gsumpt  19876  gsumxp  19890  dmdprdd  19915  dprdfadd  19936  dprdres  19944  dprdz  19946  dprdsn  19952  dprddisj2  19955  dprd2da  19958  dprd2d2  19960  dmdprdsplit2lem  19961  dpjcntz  19968  dpjdisj  19969  dpjlsm  19970  dpjidcl  19974  ablfacrp  19982  ablfac1eu  19989  pgpfac1lem1  19990  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem5  19995  pgpfaclem2  19998  acsfn1p  20719  lsssn0  20886  lss0ss  20887  lsptpcl  20917  lspsnvsi  20942  lspun0  20949  pwssplit1  20998  lsmpr  21028  lsppr  21032  lspsntri  21036  lspsolvlem  21084  lspsolv  21085  lsppratlem1  21089  lsppratlem3  21091  lsppratlem4  21092  islbs3  21097  lbsextlem4  21103  rnglidl0  21171  rsp1  21179  lidlnz  21184  lidldvgen  21276  mulgrhm2  21420  zndvds  21491  psrlidm  21904  psrridm  21905  mplmonmul  21976  mdetdiaglem  22518  mdetrlin  22522  mdetrsca  22523  mdetrsca2  22524  mdetrlin2  22527  mdetunilem5  22536  mdetunilem9  22540  mdetmul  22543  en2top  22905  rest0  23089  ordtrest  23122  iscnp4  23183  cnconst2  23203  cnpdis  23213  ist1-2  23267  cnt1  23270  dishaus  23302  discmp  23318  cmpcld  23322  conncompid  23351  dis2ndc  23380  dislly  23417  dissnref  23448  comppfsc  23452  llycmpkgen2  23470  cmpkgen  23471  1stckgenlem  23473  1stckgen  23474  ptbasfi  23501  txdis  23552  txdis1cn  23555  txcmplem1  23561  xkohaus  23573  xkoptsub  23574  xkoinjcn  23607  snfbas  23786  trnei  23812  isufil2  23828  ufileu  23839  filufint  23840  uffixsn  23845  ufildom1  23846  flimopn  23895  hausflim  23901  flimcf  23902  flimclslem  23904  flimsncls  23906  cnpflf2  23920  cnpflf  23921  fclsneii  23937  fclsfnflim  23947  fcfnei  23955  flfcntr  23963  alexsubALTlem3  23969  alexsubALTlem4  23970  ptcmplem2  23973  cldsubg  24031  snclseqg  24036  qustgphaus  24043  tsmsgsum  24059  tsmsid  24060  tgptsmscld  24071  tsmsxplem1  24073  tsmsxplem2  24074  ust0  24140  ustuqtop1  24162  neipcfilu  24216  prdsdsf  24288  prdsxmetlem  24289  prdsmet  24291  imasdsf1olem  24294  xpsdsval  24302  prdsbl  24412  prdsxmslem2  24450  idnghm  24664  icccmplem2  24745  metnrmlem2  24782  ioombl  25499  volivth  25541  itg11  25625  i1fmulclem  25636  itg2mulclem  25680  itgsplitioo  25772  limcvallem  25805  limcdif  25810  ellimc2  25811  limcflf  25815  limcmpt2  25818  limcres  25820  cnplimc  25821  limccnp  25825  limccnp2  25826  limcco  25827  dvreslem  25843  dvaddbr  25873  dvmulbr  25874  dvmulbrOLD  25875  dvcmulf  25881  dvef  25917  dvivth  25948  lhop2  25953  lhop  25954  ply1remlem  26103  fta1blem  26109  ig1peu  26113  ig1pdvds  26118  plyco0  26130  elply2  26134  plyf  26136  elplyr  26139  elplyd  26140  ply1term  26142  ply0  26146  plyeq0lem  26148  plyeq0  26149  plypf1  26150  plyaddlem  26153  plymullem  26154  dgrlem  26167  coef2  26169  coeidlem  26175  plyco  26179  coemulhi  26192  plycj  26216  plycjOLD  26218  vieta1  26253  taylf  26301  radcnv0  26358  abelth  26384  rlimcnp  26908  xrlimcnp  26911  amgm  26934  wilthlem2  27012  basellem7  27030  basellem9  27032  ppiprm  27094  chtprm  27096  musumsum  27135  muinv  27136  logexprlim  27169  perfectlem2  27174  dchrhash  27215  rpvmasum2  27456  ssltsn  27738  slerec  27765  eqscut3  27770  cofcutr  27872  cutlt  27880  cutmax  27882  cutmin  27883  addsuniflem  27948  negsunif  28001  ssltmul1  28090  ssltmul2  28091  precsexlem11  28159  onscutlt  28205  n0sfincut  28286  0reno  28401  axlowdimlem7  28928  axlowdimlem10  28931  upgrex  29072  upgr1elem  29092  uvtxnm1nbgr  29384  umgr2v2e  29506  cyclnumvtx  29780  0oo  30768  sh0le  31419  disjiunel  32575  preimane  32644  fnpreimac  32645  fsuppinisegfi  32660  fprodeq02  32798  s1f1  32914  gsumzresunsn  33039  gsumhashmul  33044  pmtrcnelor  33063  primefldgen1  33287  dvdsrspss  33351  elgrplsmsn  33354  lsmsnorb  33355  grplsm0l  33367  grplsmid  33368  0ringidl  33385  unitpidl1  33388  elrspunsn  33393  drngidl  33397  isprmidlc  33411  qsidomlem2  33417  ssdifidlprm  33422  mxidlprm  33434  mxidlirredi  33435  mxidlirred  33436  drngmxidl  33441  drngmxidlr  33442  qsdrngilem  33458  rsprprmprmidl  33486  rprmirredb  33496  1arithufdlem4  33511  lsatdim  33606  drngdimgt0  33607  dimkerim  33616  evls1fldgencl  33658  algextdeglem1  33700  algextdeglem2  33701  algextdeglem3  33702  algextdeglem4  33703  algextdeglem5  33704  rtelextdg2  33710  constrextdg2lem  33731  constrext2chnlem  33733  constrfiss  33734  qtopt1  33818  locfinref  33824  zarcls0  33851  zarmxt1  33863  zarcmplem  33864  ordtrestNEW  33904  esumsnf  34047  esum2dlem  34075  rossros  34163  oms0  34281  carsggect  34302  eulerpartlems  34344  eulerpartlemgc  34346  eulerpartlemgh  34362  eulerpartlemgs2  34364  plymulx0  34531  circlemeth  34624  hgt750lemb  34640  hgt750leme  34642  bnj1452  35035  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  36341  topjoin  36346  fnejoin2  36350  weiunse  36449  pibt2  37398  lindsadd  37600  poimirlem3  37610  poimirlem9  37616  poimirlem28  37635  poimirlem32  37639  prdsbnd  37780  heiborlem8  37805  rrnequiv  37822  grpokerinj  37880  0idl  38012  prnc  38054  isfldidl  38055  lshpnel2N  38971  lsatfixedN  38995  lfl0f  39055  lkrlsp3  39090  elpaddatriN  39790  elpaddat  39791  elpadd2at  39793  pmodlem1  39833  osumcllem1N  39943  osumcllem2N  39944  osumcllem9N  39951  osumcllem10N  39952  pexmidlem6N  39962  pexmidlem7N  39963  dibss  41156  dochocsn  41368  dochsncom  41369  dochnel  41380  dihprrnlem1N  41411  dihprrnlem2  41412  djhlsmat  41414  dihsmsprn  41417  dvh4dimlem  41430  dvhdimlem  41431  dochsnnz  41437  dochsatshp  41438  dochsnshp  41440  dochexmid  41455  dochsnkr  41459  dochsnkr2cl  41461  dochfl1  41463  lcfl7lem  41486  lcfl6  41487  lcfl8  41489  lcfl9a  41492  lclkrlem2a  41494  lclkrlem2c  41496  lclkrlem2d  41497  lclkrlem2e  41498  lclkrlem2j  41503  lclkrlem2o  41508  lclkrlem2p  41509  lclkrlem2s  41512  lclkrlem2v  41515  lcfrlem14  41543  lcfrlem18  41547  lcfrlem19  41548  lcfrlem20  41549  lcfrlem23  41552  lcfrlem25  41554  lcdlkreqN  41609  mapdval4N  41619  mapdsn  41628  mapdhvmap  41756  hdmaprnlem4tN  41839  hdmapinvlem1  41905  hdmapinvlem2  41906  hdmapinvlem3  41907  hdmapinvlem4  41908  hdmapglem5  41909  hgmapvvlem3  41912  hdmapglem7a  41914  hdmapglem7b  41915  hdmapglem7  41916  hdmapoc  41918  aks6d1c5lem3  42118  deg1gprod  42121  sticksstones9  42135  sticksstones11  42137  rhmqusspan  42166  evlsbagval  42547  selvvvval  42566  0prjspnrel  42608  elrfi  42675  cmpfiiin  42678  mzpcompact2lem  42732  dfac11  43044  pwssplit4  43071  rngunsnply  43151  flcidc  43152  proot1mul  43176  iocinico  43194  cantnfresb  43306  iunrelexp0  43684  frege81d  43729  k0004lem3  44131  mnuunid  44259  binomcxplemnn0  44331  islptre  45610  limciccioolb  45612  limcicciooub  45628  limcresiooub  45633  limcresioolb  45634  ioccncflimc  45876  icccncfext  45878  icocncflimc  45880  cncfiooicc  45885  dvnprodlem2  45938  dirkercncflem2  46095  dirkercncflem3  46096  fourierdlem48  46145  fourierdlem49  46146  fourierdlem79  46176  fourierdlem101  46198  sge0sup  46382  hoidmvlelem2  46587  hoiqssbl  46616  hspmbllem1  46617  hspmbllem2  46618  ovnovollem1  46647  fsumsplitsndif  47367  imaelsetpreimafv  47389  perfectALTVlem2  47716  stgrclnbgr0  47957  isubgr3stgrlem3  47960  1hegrlfgr  48113  gsumdifsndf  48162  sepfsepc  48909  discsubc  49046  iinfconstbas  49048