Theorem snssd 4694

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

Syntax hints:   → wi 4   ∈ wcel 2113   ⊆ wss 3841  {csn 4513

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3399  df-in 3848  df-ss 3858  df-sn 4514

This theorem is referenced by:  sofld  6013  fsnex  7044  fr3nr  7507  wfrlem15  7991  oeeui  8252  ecinxp  8396  ralxpmap  8499  xpdom3  8657  domunsn  8710  mapdom3  8732  pwfilem  8768  isinf  8803  ac6sfi  8829  pwfilemOLD  8884  finsschain  8897  ssfii  8949  marypha1lem  8963  unxpwdom2  9118  en2other2  9502  fseqenlem1  9517  axdc3lem4  9946  axdc4lem  9948  ttukeylem7  10008  fpwwe2lem12  10135  canthwe  10144  canthp1lem1  10145  wuncval2  10240  un0addcl  12002  un0mulcl  12003  ssfzunsnext  13036  fseq1p1m1  13065  hashbclem  13895  hashf1lem1  13899  hashf1lem1OLD  13900  fsumge1  15238  incexclem  15277  isumltss  15289  fprodsplit1f  15429  rpnnen2lem11  15662  bitsinv1  15878  lcmfunsnlem2  16074  lcmfass  16080  phicl2  16198  vdwlem1  16410  vdwlem8  16417  vdwlem12  16421  vdwlem13  16422  0ram  16449  ramub1lem1  16455  ramub1lem2  16456  ramcl  16458  imasaddfnlem  16897  imasaddflem  16899  imasvscafn  16906  imasvscaf  16908  mrieqvlemd  16996  mreexmrid  17010  mreexexlem4d  17014  acsfiindd  17896  acsmapd  17897  gsumress  18001  0subm  18091  gsumvallem2  18107  0subg  18415  trivsubgd  18416  trivsubgsnd  18417  trivnsgd  18435  cycsubg2cl  18465  pmtrprfv  18692  odf1o1  18808  gex1  18827  sylow2alem1  18853  sylow2alem2  18854  lsm01  18908  lsm02  18909  lsmdisj  18918  lsmdisj2  18919  prmcyg  19126  gsumzadd  19154  gsumconst  19166  gsumdifsnd  19193  gsumpt  19194  gsumxp  19208  dmdprdd  19233  dprdfadd  19254  dprdres  19262  dprdz  19264  dprdsn  19270  dprddisj2  19273  dprd2da  19276  dprd2d2  19278  dmdprdsplit2lem  19279  dpjcntz  19286  dpjdisj  19287  dpjlsm  19288  dpjidcl  19292  ablfacrp  19300  ablfac1eu  19307  pgpfac1lem1  19308  pgpfac1lem3a  19310  pgpfac1lem3  19311  pgpfac1lem5  19313  pgpfaclem2  19316  kerf1ghm  19610  acsfn1p  19690  lsssn0  19831  lss0ss  19832  lsptpcl  19863  lspsnvsi  19888  lspun0  19895  pwssplit1  19943  lsmpr  19973  lsppr  19977  lspsntri  19981  lspsolvlem  20026  lspsolv  20027  lsppratlem1  20031  lsppratlem3  20033  lsppratlem4  20034  islbs3  20039  lbsextlem4  20045  rsp1  20109  lidlnz  20113  lidldvgen  20140  mulgrhm2  20312  zndvds  20361  psrlidm  20775  psrridm  20776  mplmonmul  20840  mdetdiaglem  21342  mdetrlin  21346  mdetrsca  21347  mdetrsca2  21348  mdetrlin2  21351  mdetunilem5  21360  mdetunilem9  21364  mdetmul  21367  en2top  21729  rest0  21913  ordtrest  21946  iscnp4  22007  cnconst2  22027  cnpdis  22037  ist1-2  22091  cnt1  22094  dishaus  22126  discmp  22142  cmpcld  22146  conncompid  22175  dis2ndc  22204  dislly  22241  dissnref  22272  comppfsc  22276  llycmpkgen2  22294  cmpkgen  22295  1stckgenlem  22297  1stckgen  22298  ptbasfi  22325  txdis  22376  txdis1cn  22379  txcmplem1  22385  xkohaus  22397  xkoptsub  22398  xkoinjcn  22431  snfbas  22610  trnei  22636  isufil2  22652  ufileu  22663  filufint  22664  uffixsn  22669  ufildom1  22670  flimopn  22719  hausflim  22725  flimcf  22726  flimclslem  22728  flimsncls  22730  cnpflf2  22744  cnpflf  22745  fclsneii  22761  fclsfnflim  22771  fcfnei  22779  flfcntr  22787  alexsubALTlem3  22793  alexsubALTlem4  22794  ptcmplem2  22797  cldsubg  22855  snclseqg  22860  qustgphaus  22867  tsmsgsum  22883  tsmsid  22884  tgptsmscld  22895  tsmsxplem1  22897  tsmsxplem2  22898  ust0  22964  ustuqtop1  22986  neipcfilu  23041  prdsdsf  23113  prdsxmetlem  23114  prdsmet  23116  imasdsf1olem  23119  xpsdsval  23127  prdsbl  23237  prdsxmslem2  23275  idnghm  23489  icccmplem2  23568  metnrmlem2  23605  ioombl  24310  volivth  24352  itg11  24436  i1fmulclem  24447  itg2mulclem  24491  itgsplitioo  24582  limcvallem  24615  limcdif  24620  ellimc2  24621  limcflf  24625  limcmpt2  24628  limcres  24630  cnplimc  24631  limccnp  24635  limccnp2  24636  limcco  24637  dvreslem  24653  dvaddbr  24682  dvmulbr  24683  dvcmulf  24689  dvef  24724  dvivth  24754  lhop2  24759  lhop  24760  ply1remlem  24907  fta1blem  24913  ig1peu  24916  ig1pdvds  24921  plyco0  24933  elply2  24937  plyf  24939  elplyr  24942  elplyd  24943  ply1term  24945  ply0  24949  plyeq0lem  24951  plyeq0  24952  plypf1  24953  plyaddlem  24956  plymullem  24957  dgrlem  24970  coef2  24972  coeidlem  24978  plyco  24982  coemulhi  24995  plycj  25018  vieta1  25052  taylf  25100  radcnv0  25155  abelth  25180  rlimcnp  25695  xrlimcnp  25698  amgm  25720  wilthlem2  25798  basellem7  25816  basellem9  25818  ppiprm  25880  chtprm  25882  musumsum  25921  muinv  25922  logexprlim  25953  perfectlem2  25958  dchrhash  25999  rpvmasum2  26240  axlowdimlem7  26886  axlowdimlem10  26889  upgrex  27029  upgr1elem  27049  uvtxnm1nbgr  27338  umgr2v2e  27459  0oo  28716  sh0le  29367  disjiunel  30501  preimane  30574  fnpreimac  30575  fsuppinisegfi  30588  fprodeq02  30704  s1f1  30784  gsumzresunsn  30883  gsumhashmul  30885  pmtrcnelor  30929  elgrplsmsn  31142  lsmsnorb  31143  grplsm0l  31155  grplsmid  31156  0ringidl  31169  isprmidlc  31187  qsidomlem2  31193  mxidlprm  31204  lsatdim  31264  drngdimgt0  31265  dimkerim  31272  qtopt1  31349  locfinref  31355  zarcls0  31382  zarmxt1  31394  zarcmplem  31395  ordtrestNEW  31435  esumsnf  31594  esum2dlem  31622  rossros  31710  oms0  31826  carsggect  31847  eulerpartlems  31889  eulerpartlemgc  31891  eulerpartlemgh  31907  eulerpartlemgs2  31909  plymulx0  32088  circlemeth  32182  hgt750lemb  32198  hgt750leme  32200  bnj1452  32595  pthhashvtx  32652  subfacp1lem1  32704  subfacp1lem5  32709  erdszelem4  32719  erdszelem8  32723  sconnpi1  32764  cvmscld  32798  cvmlift2lem6  32833  cvmlift2lem9  32836  cvmlift2lem11  32838  cvmlift2lem12  32839  mrsubvrs  33047  frrlem13  33445  slerec  33646  cofcutr  33722  neibastop2lem  34179  topjoin  34184  fnejoin2  34188  pibt2  35200  lindsadd  35382  poimirlem3  35392  poimirlem9  35398  poimirlem28  35417  poimirlem32  35421  prdsbnd  35563  heiborlem8  35588  rrnequiv  35605  grpokerinj  35663  0idl  35795  prnc  35837  isfldidl  35838  lshpnel2N  36611  lsatfixedN  36635  lfl0f  36695  lkrlsp3  36730  elpaddatriN  37429  elpaddat  37430  elpadd2at  37432  pmodlem1  37472  osumcllem1N  37582  osumcllem2N  37583  osumcllem9N  37590  osumcllem10N  37591  pexmidlem6N  37601  pexmidlem7N  37602  dibss  38795  dochocsn  39007  dochsncom  39008  dochnel  39019  dihprrnlem1N  39050  dihprrnlem2  39051  djhlsmat  39053  dihsmsprn  39056  dvh4dimlem  39069  dvhdimlem  39070  dochsnnz  39076  dochsatshp  39077  dochsnshp  39079  dochexmid  39094  dochsnkr  39098  dochsnkr2cl  39100  dochfl1  39102  lcfl7lem  39125  lcfl6  39126  lcfl8  39128  lcfl9a  39131  lclkrlem2a  39133  lclkrlem2c  39135  lclkrlem2d  39136  lclkrlem2e  39137  lclkrlem2j  39142  lclkrlem2o  39147  lclkrlem2p  39148  lclkrlem2s  39151  lclkrlem2v  39154  lcfrlem14  39182  lcfrlem18  39186  lcfrlem19  39187  lcfrlem20  39188  lcfrlem23  39191  lcfrlem25  39193  lcdlkreqN  39248  mapdval4N  39258  mapdsn  39267  mapdhvmap  39395  hdmaprnlem4tN  39478  hdmapinvlem1  39544  hdmapinvlem2  39545  hdmapinvlem3  39546  hdmapinvlem4  39547  hdmapglem5  39548  hgmapvvlem3  39551  hdmapglem7a  39553  hdmapglem7b  39554  hdmapglem7  39555  hdmapoc  39557  evlsbagval  39838  0prjspnrel  40025  elrfi  40072  cmpfiiin  40075  mzpcompact2lem  40129  dfac11  40443  pwssplit4  40470  rngunsnply  40554  flcidc  40555  proot1mul  40580  iocinico  40599  iunrelexp0  40840  frege81d  40885  k0004lem3  41289  mnuunid  41421  binomcxplemnn0  41489  fsumsplit1  42639  islptre  42686  limciccioolb  42688  limcicciooub  42704  limcresiooub  42709  limcresioolb  42710  ioccncflimc  42952  icccncfext  42954  icocncflimc  42956  cncfiooicc  42961  dvnprodlem2  43014  dirkercncflem2  43171  dirkercncflem3  43172  fourierdlem48  43221  fourierdlem49  43222  fourierdlem79  43252  fourierdlem101  43274  sge0sup  43455  hoidmvlelem2  43660  hoiqssbl  43689  hspmbllem1  43690  hspmbllem2  43691  ovnovollem1  43720  fsumsplitsndif  44343  imaelsetpreimafv  44365  perfectALTVlem2  44692  1hegrlfgr  44812  gsumdifsndf  44893  sepfsepc  45727