Theorem snssd 4753

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

Syntax hints:   → wi 4   ∈ wcel 2114   ⊆ wss 3890  {csn 4568

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-ss 3907  df-sn 4569

This theorem is referenced by:  intidg  5405  sofld  6146  fsnex  7232  fr3nr  7720  resf1extb  7879  resf1ext2b  7880  frrlem13  8242  oeeui  8532  naddunif  8623  naddasslem1  8624  naddasslem2  8625  ecinxp  8733  ralxpmap  8838  xpdom3  9007  domunsn  9059  mapdom3  9081  isinf  9169  ac6sfi  9188  pwfilem  9222  finsschain  9263  ssfii  9326  marypha1lem  9340  unxpwdom2  9497  en2other2  9925  fseqenlem1  9940  axdc3lem4  10369  axdc4lem  10371  ttukeylem7  10431  fpwwe2lem12  10559  canthwe  10568  canthp1lem1  10569  wuncval2  10664  un0addcl  12464  un0mulcl  12465  ssfzunsnext  13517  fseq1p1m1  13546  hashbclem  14408  hashf1lem1  14411  fsumsplit1  15701  fsumge1  15754  incexclem  15795  isumltss  15807  fprodsplit1f  15949  rpnnen2lem11  16185  bitsinv1  16405  lcmfunsnlem2  16603  lcmfass  16609  phicl2  16732  vdwlem1  16946  vdwlem8  16953  vdwlem12  16957  vdwlem13  16958  0ram  16985  ramub1lem1  16991  ramub1lem2  16992  ramcl  16994  imasaddfnlem  17486  imasaddflem  17488  imasvscafn  17495  imasvscaf  17497  mrieqvlemd  17589  mreexmrid  17603  mreexexlem4d  17607  acsfiindd  18513  acsmapd  18514  chnccat  18586  gsumress  18644  0subm  18779  gsumvallem2  18796  trivsubgd  19122  trivsubgsnd  19123  trivnsgd  19141  cycsubg2cl  19180  kerf1ghm  19216  pmtrprfv  19422  odf1o1  19541  gex1  19560  sylow2alem1  19586  sylow2alem2  19587  lsm01  19640  lsm02  19641  lsmdisj  19650  lsmdisj2  19651  prmcyg  19863  gsumzadd  19891  gsumconst  19903  gsumdifsnd  19930  gsumpt  19931  gsumxp  19945  dmdprdd  19970  dprdfadd  19991  dprdres  19999  dprdz  20001  dprdsn  20007  dprddisj2  20010  dprd2da  20013  dprd2d2  20015  dmdprdsplit2lem  20016  dpjcntz  20023  dpjdisj  20024  dpjlsm  20025  dpjidcl  20029  ablfacrp  20037  ablfac1eu  20044  pgpfac1lem1  20045  pgpfac1lem3a  20047  pgpfac1lem3  20048  pgpfac1lem5  20050  pgpfaclem2  20053  acsfn1p  20770  lsssn0  20937  lss0ss  20938  lsptpcl  20968  lspsnvsi  20993  lspun0  21000  pwssplit1  21049  lsmpr  21079  lsppr  21083  lspsntri  21087  lspsolvlem  21135  lspsolv  21136  lsppratlem1  21140  lsppratlem3  21142  lsppratlem4  21143  islbs3  21148  lbsextlem4  21154  rnglidl0  21222  rsp1  21230  lidlnz  21235  lidldvgen  21327  mulgrhm2  21471  zndvds  21542  psrlidm  21953  psrridm  21954  mplmonmul  22027  mdetdiaglem  22576  mdetrlin  22580  mdetrsca  22581  mdetrsca2  22582  mdetrlin2  22585  mdetunilem5  22594  mdetunilem9  22598  mdetmul  22601  en2top  22963  rest0  23147  ordtrest  23180  iscnp4  23241  cnconst2  23261  cnpdis  23271  ist1-2  23325  cnt1  23328  dishaus  23360  discmp  23376  cmpcld  23380  conncompid  23409  dis2ndc  23438  dislly  23475  dissnref  23506  comppfsc  23510  llycmpkgen2  23528  cmpkgen  23529  1stckgenlem  23531  1stckgen  23532  ptbasfi  23559  txdis  23610  txdis1cn  23613  txcmplem1  23619  xkohaus  23631  xkoptsub  23632  xkoinjcn  23665  snfbas  23844  trnei  23870  isufil2  23886  ufileu  23897  filufint  23898  uffixsn  23903  ufildom1  23904  flimopn  23953  hausflim  23959  flimcf  23960  flimclslem  23962  flimsncls  23964  cnpflf2  23978  cnpflf  23979  fclsneii  23995  fclsfnflim  24005  fcfnei  24013  flfcntr  24021  alexsubALTlem3  24027  alexsubALTlem4  24028  ptcmplem2  24031  cldsubg  24089  snclseqg  24094  qustgphaus  24101  tsmsgsum  24117  tsmsid  24118  tgptsmscld  24129  tsmsxplem1  24131  tsmsxplem2  24132  ust0  24198  ustuqtop1  24219  neipcfilu  24273  prdsdsf  24345  prdsxmetlem  24346  prdsmet  24348  imasdsf1olem  24351  xpsdsval  24359  prdsbl  24469  prdsxmslem2  24507  idnghm  24721  icccmplem2  24802  metnrmlem2  24839  ioombl  25545  volivth  25587  itg11  25671  i1fmulclem  25682  itg2mulclem  25726  itgsplitioo  25818  limcvallem  25851  limcdif  25856  ellimc2  25857  limcflf  25861  limcmpt2  25864  limcres  25866  cnplimc  25867  limccnp  25871  limccnp2  25872  limcco  25873  dvreslem  25889  dvaddbr  25918  dvmulbr  25919  dvcmulf  25925  dvef  25960  dvivth  25990  lhop2  25995  lhop  25996  ply1remlem  26143  fta1blem  26149  ig1peu  26153  ig1pdvds  26158  plyco0  26170  elply2  26174  plyf  26176  elplyr  26179  elplyd  26180  ply1term  26182  ply0  26186  plyeq0lem  26188  plyeq0  26189  plypf1  26190  plyaddlem  26193  plymullem  26194  dgrlem  26207  coef2  26209  coeidlem  26215  plyco  26219  coemulhi  26232  plycj  26255  plycjOLD  26257  vieta1  26292  taylf  26340  radcnv0  26397  abelth  26422  rlimcnp  26945  xrlimcnp  26948  amgm  26971  wilthlem2  27049  basellem7  27067  basellem9  27069  ppiprm  27131  chtprm  27133  musumsum  27172  muinv  27173  logexprlim  27205  perfectlem2  27210  dchrhash  27251  rpvmasum2  27492  sltssnb  27778  lesrec  27808  eqcuts3  27813  cofcutr  27933  cutlt  27941  cutmax  27943  cutmin  27944  cutminmax  27945  addsuniflem  28010  negsunif  28064  sltmuls1  28156  sltmuls2  28157  precsexlem11  28226  oncutlt  28273  n0fincut  28364  bdaypw2n0bndlem  28472  axlowdimlem7  29034  axlowdimlem10  29037  upgrex  29178  upgr1elem  29198  uvtxnm1nbgr  29490  umgr2v2e  29612  cyclnumvtx  29886  0oo  30878  sh0le  31529  disjiunel  32684  preimane  32760  fnpreimac  32761  fsuppinisegfi  32778  fprodeq02  32915  indsn  32941  s1f1  33021  gsumzresunsn  33141  gsumhashmul  33146  pmtrcnelor  33170  primefldgen1  33400  dvdsrspss  33465  elgrplsmsn  33468  lsmsnorb  33469  grplsm0l  33481  grplsmid  33482  0ringidl  33499  unitpidl1  33502  elrspunsn  33507  drngidl  33511  isprmidlc  33525  qsidomlem2  33531  ssdifidlprm  33536  mxidlprm  33548  mxidlirredi  33549  mxidlirred  33550  drngmxidl  33555  drngmxidlr  33556  qsdrngilem  33572  rsprprmprmidl  33600  rprmirredb  33610  1arithufdlem4  33625  mvrvalind  33700  mplmulmvr  33701  evlextv  33704  psrmonmul  33712  esplyfval0  33726  esplyfvaln  33736  esplyind  33737  esplyindfv  33738  vietalem  33741  lsatdim  33780  drngdimgt0  33781  dimkerim  33790  evls1fldgencl  33833  algextdeglem1  33880  algextdeglem2  33881  algextdeglem3  33882  algextdeglem4  33883  algextdeglem5  33884  rtelextdg2  33890  constrextdg2lem  33911  constrext2chnlem  33913  constrfiss  33914  qtopt1  33998  locfinref  34004  zarcls0  34031  zarmxt1  34043  zarcmplem  34044  ordtrestNEW  34084  esumsnf  34227  esum2dlem  34255  rossros  34343  oms0  34460  carsggect  34481  eulerpartlems  34523  eulerpartlemgc  34525  eulerpartlemgh  34541  eulerpartlemgs2  34543  plymulx0  34710  circlemeth  34803  hgt750lemb  34819  hgt750leme  34821  bnj1452  35213  pthhashvtx  35329  subfacp1lem1  35380  subfacp1lem5  35385  erdszelem4  35395  erdszelem8  35399  sconnpi1  35440  cvmscld  35474  cvmlift2lem6  35509  cvmlift2lem9  35512  cvmlift2lem11  35514  cvmlift2lem12  35515  mrsubvrs  35723  ellcsrspsn  35842  neibastop2lem  36561  topjoin  36566  fnejoin2  36570  weiunse  36669  pibt2  37750  lindsadd  37951  poimirlem3  37961  poimirlem9  37967  poimirlem28  37986  poimirlem32  37990  prdsbnd  38131  heiborlem8  38156  rrnequiv  38173  grpokerinj  38231  0idl  38363  prnc  38405  isfldidl  38406  lshpnel2N  39448  lsatfixedN  39472  lfl0f  39532  lkrlsp3  39567  elpaddatriN  40266  elpaddat  40267  elpadd2at  40269  pmodlem1  40309  osumcllem1N  40419  osumcllem2N  40420  osumcllem9N  40427  osumcllem10N  40428  pexmidlem6N  40438  pexmidlem7N  40439  dibss  41632  dochocsn  41844  dochsncom  41845  dochnel  41856  dihprrnlem1N  41887  dihprrnlem2  41888  djhlsmat  41890  dihsmsprn  41893  dvh4dimlem  41906  dvhdimlem  41907  dochsnnz  41913  dochsatshp  41914  dochsnshp  41916  dochexmid  41931  dochsnkr  41935  dochsnkr2cl  41937  dochfl1  41939  lcfl7lem  41962  lcfl6  41963  lcfl8  41965  lcfl9a  41968  lclkrlem2a  41970  lclkrlem2c  41972  lclkrlem2d  41973  lclkrlem2e  41974  lclkrlem2j  41979  lclkrlem2o  41984  lclkrlem2p  41985  lclkrlem2s  41988  lclkrlem2v  41991  lcfrlem14  42019  lcfrlem18  42023  lcfrlem19  42024  lcfrlem20  42025  lcfrlem23  42028  lcfrlem25  42030  lcdlkreqN  42085  mapdval4N  42095  mapdsn  42104  mapdhvmap  42232  hdmaprnlem4tN  42315  hdmapinvlem1  42381  hdmapinvlem2  42382  hdmapinvlem3  42383  hdmapinvlem4  42384  hdmapglem5  42385  hgmapvvlem3  42388  hdmapglem7a  42390  hdmapglem7b  42391  hdmapglem7  42392  hdmapoc  42394  aks6d1c5lem3  42593  deg1gprod  42596  sticksstones9  42610  sticksstones11  42612  rhmqusspan  42641  evlsbagval  43019  selvvvval  43035  0prjspnrel  43077  elrfi  43143  cmpfiiin  43146  mzpcompact2lem  43200  dfac11  43511  pwssplit4  43538  rngunsnply  43618  flcidc  43619  proot1mul  43643  iocinico  43661  cantnfresb  43773  iunrelexp0  44150  frege81d  44195  k0004lem3  44597  mnuunid  44725  binomcxplemnn0  44797  islptre  46070  limciccioolb  46072  limcicciooub  46086  limcresiooub  46091  limcresioolb  46092  ioccncflimc  46334  icccncfext  46336  icocncflimc  46338  cncfiooicc  46343  dvnprodlem2  46396  dirkercncflem2  46553  dirkercncflem3  46554  fourierdlem48  46603  fourierdlem49  46604  fourierdlem79  46634  fourierdlem101  46656  sge0sup  46840  hoidmvlelem2  47045  hoiqssbl  47074  hspmbllem1  47075  hspmbllem2  47076  ovnovollem1  47105  fsumsplitsndif  47844  imaelsetpreimafv  47870  perfectALTVlem2  48213  stgrclnbgr0  48456  isubgr3stgrlem3  48459  1hegrlfgr  48623  gsumdifsndf  48672  sepfsepc  49418  discsubc  49554  iinfconstbas  49556