Theorem snssd 4804

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

Syntax hints:   → wi 4   ∈ wcel 2098   ⊆ wss 3940  {csn 4620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3947  df-ss 3957  df-sn 4621

This theorem is referenced by:  intidg  5447  sofld  6176  fsnex  7273  fr3nr  7752  frrlem13  8278  wfrlem15OLD  8318  oeeui  8597  naddunif  8688  naddasslem1  8689  naddasslem2  8690  ecinxp  8782  ralxpmap  8886  xpdom3  9066  domunsn  9123  mapdom3  9145  pwfilem  9173  isinf  9256  isinfOLD  9257  ac6sfi  9283  pwfilemOLD  9342  finsschain  9355  ssfii  9410  marypha1lem  9424  unxpwdom2  9579  en2other2  10000  fseqenlem1  10015  axdc3lem4  10444  axdc4lem  10446  ttukeylem7  10506  fpwwe2lem12  10633  canthwe  10642  canthp1lem1  10643  wuncval2  10738  un0addcl  12502  un0mulcl  12503  ssfzunsnext  13543  fseq1p1m1  13572  hashbclem  14408  hashf1lem1  14412  hashf1lem1OLD  14413  fsumsplit1  15688  fsumge1  15740  incexclem  15779  isumltss  15791  fprodsplit1f  15931  rpnnen2lem11  16164  bitsinv1  16380  lcmfunsnlem2  16574  lcmfass  16580  phicl2  16700  vdwlem1  16913  vdwlem8  16920  vdwlem12  16924  vdwlem13  16925  0ram  16952  ramub1lem1  16958  ramub1lem2  16959  ramcl  16961  imasaddfnlem  17473  imasaddflem  17475  imasvscafn  17482  imasvscaf  17484  mrieqvlemd  17572  mreexmrid  17586  mreexexlem4d  17590  acsfiindd  18508  acsmapd  18509  gsumress  18605  0subm  18732  gsumvallem2  18749  0subgOLD  19069  trivsubgd  19070  trivsubgsnd  19071  trivnsgd  19089  cycsubg2cl  19127  kerf1ghm  19162  pmtrprfv  19363  odf1o1  19482  gex1  19501  sylow2alem1  19527  sylow2alem2  19528  lsm01  19581  lsm02  19582  lsmdisj  19591  lsmdisj2  19592  prmcyg  19804  gsumzadd  19832  gsumconst  19844  gsumdifsnd  19871  gsumpt  19872  gsumxp  19886  dmdprdd  19911  dprdfadd  19932  dprdres  19940  dprdz  19942  dprdsn  19948  dprddisj2  19951  dprd2da  19954  dprd2d2  19956  dmdprdsplit2lem  19957  dpjcntz  19964  dpjdisj  19965  dpjlsm  19966  dpjidcl  19970  ablfacrp  19978  ablfac1eu  19985  pgpfac1lem1  19986  pgpfac1lem3a  19988  pgpfac1lem3  19989  pgpfac1lem5  19991  pgpfaclem2  19994  acsfn1p  20640  lsssn0  20785  lss0ss  20786  lsptpcl  20816  lspsnvsi  20841  lspun0  20848  pwssplit1  20897  lsmpr  20927  lsppr  20931  lspsntri  20935  lspsolvlem  20983  lspsolv  20984  lsppratlem1  20988  lsppratlem3  20990  lsppratlem4  20991  islbs3  20996  lbsextlem4  21002  rnglidl0  21078  rsp1  21086  lidlnz  21090  lidldvgen  21177  mulgrhm2  21333  zndvds  21412  psrlidm  21833  psrridm  21834  mplmonmul  21901  mdetdiaglem  22422  mdetrlin  22426  mdetrsca  22427  mdetrsca2  22428  mdetrlin2  22431  mdetunilem5  22440  mdetunilem9  22444  mdetmul  22447  en2top  22810  rest0  22995  ordtrest  23028  iscnp4  23089  cnconst2  23109  cnpdis  23119  ist1-2  23173  cnt1  23176  dishaus  23208  discmp  23224  cmpcld  23228  conncompid  23257  dis2ndc  23286  dislly  23323  dissnref  23354  comppfsc  23358  llycmpkgen2  23376  cmpkgen  23377  1stckgenlem  23379  1stckgen  23380  ptbasfi  23407  txdis  23458  txdis1cn  23461  txcmplem1  23467  xkohaus  23479  xkoptsub  23480  xkoinjcn  23513  snfbas  23692  trnei  23718  isufil2  23734  ufileu  23745  filufint  23746  uffixsn  23751  ufildom1  23752  flimopn  23801  hausflim  23807  flimcf  23808  flimclslem  23810  flimsncls  23812  cnpflf2  23826  cnpflf  23827  fclsneii  23843  fclsfnflim  23853  fcfnei  23861  flfcntr  23869  alexsubALTlem3  23875  alexsubALTlem4  23876  ptcmplem2  23879  cldsubg  23937  snclseqg  23942  qustgphaus  23949  tsmsgsum  23965  tsmsid  23966  tgptsmscld  23977  tsmsxplem1  23979  tsmsxplem2  23980  ust0  24046  ustuqtop1  24068  neipcfilu  24123  prdsdsf  24195  prdsxmetlem  24196  prdsmet  24198  imasdsf1olem  24201  xpsdsval  24209  prdsbl  24322  prdsxmslem2  24360  idnghm  24582  icccmplem2  24661  metnrmlem2  24698  ioombl  25416  volivth  25458  itg11  25542  i1fmulclem  25554  itg2mulclem  25598  itgsplitioo  25689  limcvallem  25722  limcdif  25727  ellimc2  25728  limcflf  25732  limcmpt2  25735  limcres  25737  cnplimc  25738  limccnp  25742  limccnp2  25743  limcco  25744  dvreslem  25760  dvaddbr  25790  dvmulbr  25791  dvmulbrOLD  25792  dvcmulf  25798  dvef  25834  dvivth  25865  lhop2  25870  lhop  25871  ply1remlem  26020  fta1blem  26026  ig1peu  26029  ig1pdvds  26034  plyco0  26046  elply2  26050  plyf  26052  elplyr  26055  elplyd  26056  ply1term  26058  ply0  26062  plyeq0lem  26064  plyeq0  26065  plypf1  26066  plyaddlem  26069  plymullem  26070  dgrlem  26083  coef2  26085  coeidlem  26091  plyco  26095  coemulhi  26108  plycj  26132  vieta1  26166  taylf  26214  radcnv0  26269  abelth  26295  rlimcnp  26813  xrlimcnp  26816  amgm  26839  wilthlem2  26917  basellem7  26935  basellem9  26937  ppiprm  26999  chtprm  27001  musumsum  27040  muinv  27041  logexprlim  27074  perfectlem2  27079  dchrhash  27120  rpvmasum2  27361  ssltsn  27641  slerec  27668  cofcutr  27760  cutlt  27768  addsuniflem  27834  negsunif  27883  ssltmul1  27963  ssltmul2  27964  precsexlem11  28031  0reno  28141  axlowdimlem7  28675  axlowdimlem10  28678  upgrex  28821  upgr1elem  28841  uvtxnm1nbgr  29130  umgr2v2e  29251  0oo  30511  sh0le  31162  disjiunel  32296  preimane  32364  fnpreimac  32365  fsuppinisegfi  32378  fprodeq02  32496  s1f1  32576  gsumzresunsn  32674  gsumhashmul  32676  pmtrcnelor  32720  primefldgen1  32877  dvdsrspss  32960  elgrplsmsn  32969  lsmsnorb  32970  grplsm0l  32982  grplsmid  32983  0ringidl  33008  unitpidl1  33011  elrspunsn  33016  drngidl  33020  isprmidlc  33035  qsidomlem2  33041  mxidlprm  33055  mxidlirredi  33056  mxidlirred  33057  drngmxidl  33062  qsdrngilem  33077  lsatdim  33181  drngdimgt0  33182  dimkerim  33191  evls1fldgencl  33224  algextdeglem1  33253  algextdeglem2  33254  algextdeglem3  33255  algextdeglem4  33256  algextdeglem5  33257  qtopt1  33304  locfinref  33310  zarcls0  33337  zarmxt1  33349  zarcmplem  33350  ordtrestNEW  33390  esumsnf  33551  esum2dlem  33579  rossros  33667  oms0  33785  carsggect  33806  eulerpartlems  33848  eulerpartlemgc  33850  eulerpartlemgh  33866  eulerpartlemgs2  33868  plymulx0  34047  circlemeth  34141  hgt750lemb  34157  hgt750leme  34159  bnj1452  34552  pthhashvtx  34607  subfacp1lem1  34659  subfacp1lem5  34664  erdszelem4  34674  erdszelem8  34678  sconnpi1  34719  cvmscld  34753  cvmlift2lem6  34788  cvmlift2lem9  34791  cvmlift2lem11  34793  cvmlift2lem12  34794  mrsubvrs  35002  neibastop2lem  35735  topjoin  35740  fnejoin2  35744  pibt2  36788  lindsadd  36971  poimirlem3  36981  poimirlem9  36987  poimirlem28  37006  poimirlem32  37010  prdsbnd  37151  heiborlem8  37176  rrnequiv  37193  grpokerinj  37251  0idl  37383  prnc  37425  isfldidl  37426  lshpnel2N  38345  lsatfixedN  38369  lfl0f  38429  lkrlsp3  38464  elpaddatriN  39164  elpaddat  39165  elpadd2at  39167  pmodlem1  39207  osumcllem1N  39317  osumcllem2N  39318  osumcllem9N  39325  osumcllem10N  39326  pexmidlem6N  39336  pexmidlem7N  39337  dibss  40530  dochocsn  40742  dochsncom  40743  dochnel  40754  dihprrnlem1N  40785  dihprrnlem2  40786  djhlsmat  40788  dihsmsprn  40791  dvh4dimlem  40804  dvhdimlem  40805  dochsnnz  40811  dochsatshp  40812  dochsnshp  40814  dochexmid  40829  dochsnkr  40833  dochsnkr2cl  40835  dochfl1  40837  lcfl7lem  40860  lcfl6  40861  lcfl8  40863  lcfl9a  40866  lclkrlem2a  40868  lclkrlem2c  40870  lclkrlem2d  40871  lclkrlem2e  40872  lclkrlem2j  40877  lclkrlem2o  40882  lclkrlem2p  40883  lclkrlem2s  40886  lclkrlem2v  40889  lcfrlem14  40917  lcfrlem18  40921  lcfrlem19  40922  lcfrlem20  40923  lcfrlem23  40926  lcfrlem25  40928  lcdlkreqN  40983  mapdval4N  40993  mapdsn  41002  mapdhvmap  41130  hdmaprnlem4tN  41213  hdmapinvlem1  41279  hdmapinvlem2  41280  hdmapinvlem3  41281  hdmapinvlem4  41282  hdmapglem5  41283  hgmapvvlem3  41286  hdmapglem7a  41288  hdmapglem7b  41289  hdmapglem7  41290  hdmapoc  41292  sticksstones9  41463  sticksstones11  41465  evlsbagval  41627  selvvvval  41646  0prjspnrel  41858  elrfi  41921  cmpfiiin  41924  mzpcompact2lem  41978  dfac11  42293  pwssplit4  42320  rngunsnply  42404  flcidc  42405  proot1mul  42430  iocinico  42450  cantnfresb  42563  iunrelexp0  42942  frege81d  42987  k0004lem3  43389  mnuunid  43525  binomcxplemnn0  43597  islptre  44820  limciccioolb  44822  limcicciooub  44838  limcresiooub  44843  limcresioolb  44844  ioccncflimc  45086  icccncfext  45088  icocncflimc  45090  cncfiooicc  45095  dvnprodlem2  45148  dirkercncflem2  45305  dirkercncflem3  45306  fourierdlem48  45355  fourierdlem49  45356  fourierdlem79  45386  fourierdlem101  45408  sge0sup  45592  hoidmvlelem2  45797  hoiqssbl  45826  hspmbllem1  45827  hspmbllem2  45828  ovnovollem1  45857  fsumsplitsndif  46526  imaelsetpreimafv  46548  perfectALTVlem2  46875  1hegrlfgr  46995  gsumdifsndf  47044  sepfsepc  47748