Theorem snssd 4752

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

Syntax hints:   → wi 4   ∈ wcel 2143   ⊆ wss 3905  {csn 4589

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-ss 3922  df-sn 4590

This theorem is referenced by:  intidg  5438  sofld  6185  fsnex  7281  fr3nr  7767  resf1extb  7927  resf1ext2b  7928  frrlem13  8291  oeeui  8584  naddunif  8676  naddasslem1  8677  naddasslem2  8678  ecinxp  8786  ralxpmap  8890  xpdom3  9059  domunsn  9111  mapdom3  9133  isinf  9221  ac6sfi  9240  pwfilem  9273  finsschain  9312  ssfii  9375  marypha1lem  9389  unxpwdom2  9546  en2other2  9989  fseqenlem1  10004  axdc3lem4  10432  axdc4lem  10434  ttukeylem7  10494  fpwwe2lem12  10622  canthwe  10631  canthp1lem1  10632  wuncval2  10727  un0addcl  12532  un0mulcl  12533  ssfzunsnext  13593  fseq1p1m1  13622  hashbclem  14485  hashf1lem1  14488  fsumsplit1  15792  fsumge1  15845  incexclem  15886  isumltss  15898  fprodsplit1f  16040  rpnnen2lem11  16275  bitsinv1  16495  lcmfunsnlem2  16693  lcmfass  16699  phicl2  16822  vdwlem1  17036  vdwlem8  17043  vdwlem12  17047  vdwlem13  17048  0ram  17075  ramub1lem1  17081  ramub1lem2  17082  ramcl  17084  imasaddfnlem  17577  imasaddflem  17579  imasvscafn  17586  imasvscaf  17588  mrieqvlemd  17680  mreexmrid  17694  mreexexlem4d  17698  acsfiindd  18604  acsmapd  18605  chnccat  18677  gsumress  18735  0subm  18871  gsumvallem2  18888  trivsubgd  19214  trivsubgsnd  19215  trivnsgd  19233  cycsubg2cl  19277  kerf1ghm  19312  pmtrprfv  19518  odf1o1  19637  gex1  19656  sylow2alem1  19682  sylow2alem2  19683  lsm01  19736  lsm02  19737  lsmdisj  19746  lsmdisj2  19747  prmcyg  19959  gsumzadd  19987  gsumconst  19999  gsumdifsnd  20026  gsumpt  20027  gsumxp  20041  dmdprdd  20066  dprdfadd  20087  dprdres  20095  dprdz  20097  dprdsn  20103  dprddisj2  20106  dprd2da  20109  dprd2d2  20111  dmdprdsplit2lem  20112  dpjcntz  20119  dpjdisj  20120  dpjlsm  20121  dpjidcl  20125  ablfacrp  20133  ablfac1eu  20140  pgpfac1lem1  20141  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfac1lem5  20146  pgpfaclem2  20149  acsfn1p  20902  lsssn0  21069  lss0ss  21070  lsptpcl  21100  lspsnvsi  21125  lspun0  21132  pwssplit1  21180  lsmpr  21210  lsppr  21214  lspsntri  21218  lspsolvlem  21266  lspsolv  21267  lsppratlem1  21271  lsppratlem3  21273  lsppratlem4  21274  islbs3  21279  lbsextlem4  21285  rnglidl0  21355  0ringidl  21360  rsp1  21366  lidlnz  21376  drngidl  21385  isprmidlc  21472  qsidomlem2  21481  ssdifidlprm  21486  lidldvgen  21502  mulgrhm2  21628  zndvds  21699  psrlidm  22111  psrridm  22112  mplmonmul  22187  selvvvval  22293  mdetdiaglem  22755  mdetrlin  22759  mdetrsca  22760  mdetrsca2  22761  mdetrlin2  22764  mdetunilem5  22773  mdetunilem9  22777  mdetmul  22780  en2top  23142  rest0  23326  ordtrest  23359  iscnp4  23420  cnconst2  23440  cnpdis  23450  ist1-2  23504  cnt1  23507  dishaus  23539  discmp  23555  cmpcld  23559  conncompid  23588  dis2ndc  23617  dislly  23654  dissnref  23685  comppfsc  23689  llycmpkgen2  23707  cmpkgen  23708  1stckgenlem  23710  1stckgen  23711  ptbasfi  23738  txdis  23789  txdis1cn  23792  txcmplem1  23798  xkohaus  23810  xkoptsub  23811  xkoinjcn  23844  snfbas  24023  trnei  24049  isufil2  24065  ufileu  24076  filufint  24077  uffixsn  24082  ufildom1  24083  flimopn  24132  hausflim  24138  flimcf  24139  flimclslem  24141  flimsncls  24143  cnpflf2  24157  cnpflf  24158  fclsneii  24174  fclsfnflim  24184  fcfnei  24192  flfcntr  24200  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem2  24210  cldsubg  24268  snclseqg  24273  qustgphaus  24280  tsmsgsum  24296  tsmsid  24297  tgptsmscld  24308  tsmsxplem1  24310  tsmsxplem2  24311  ust0  24377  ustuqtop1  24398  neipcfilu  24452  prdsdsf  24524  prdsxmetlem  24525  prdsmet  24527  imasdsf1olem  24530  xpsdsval  24538  prdsbl  24648  prdsxmslem2  24686  idnghm  24900  icccmplem2  24981  metnrmlem2  25018  ioombl  25724  volivth  25766  itg11  25850  i1fmulclem  25861  itg2mulclem  25905  itgsplitioo  25997  limcvallem  26030  limcdif  26035  ellimc2  26036  limcflf  26040  limcmpt2  26043  limcres  26045  cnplimc  26046  limccnp  26050  limccnp2  26051  limcco  26052  dvreslem  26068  dvaddbr  26097  dvmulbr  26098  dvcmulf  26104  dvef  26139  dvivth  26169  lhop2  26174  lhop  26175  ply1remlem  26322  fta1blem  26328  ig1peu  26332  ig1pdvds  26337  plyco0  26349  elply2  26353  plyf  26355  elplyr  26358  elplyd  26359  ply1term  26361  ply0  26365  plyeq0lem  26367  plyeq0  26368  plypf1  26369  plyaddlem  26372  plymullem  26373  dgrlem  26386  coef2  26388  coeidlem  26394  plyco  26398  coemulhi  26411  plycj  26434  plycjOLD  26436  plyn0mulidp  26442  vieta1  26473  taylf  26524  radcnv0  26579  abelth  26604  rlimcnp  27130  xrlimcnp  27133  amgm  27155  wilthlem2  27233  basellem7  27251  basellem9  27253  ppiprm  27315  chtprm  27317  musumsum  27356  muinv  27357  logexprlim  27389  perfectlem2  27394  dchrhash  27435  rpvmasum2  27676  sltssnb  27962  conway  27972  lesrec  27992  eqcuts3  27997  cofcutr  28117  cutlt  28125  cutmax  28127  cutmin  28128  cutminmax  28129  addsuniflem  28194  negsunif  28248  sltmuls1  28340  sltmuls2  28341  precsexlem11  28410  oncutlt  28457  n0fincut  28548  bdaypw2n0bndlem  28656  axlowdimlem7  29298  axlowdimlem10  29301  upgrex  29442  upgr1elem  29462  uvtxnm1nbgr  29754  umgr2v2e  29875  cyclnumvtx  30149  0oo  31141  sh0le  31792  disjiunel  32941  preimane  33014  fnpreimac  33015  fsuppinisegfi  33032  fprodeq02  33168  indsn  33183  s1f1  33263  gsumzresunsn  33382  gsumhashmul  33387  pmtrcnelor  33411  primefldgen1  33642  dvdsrspss  33700  elgrplsmsn  33703  lsmsnorb  33704  grplsm0l  33712  grplsmid  33713  unitpidl1  33732  elrspunsn  33737  mxidlprm  33753  mxidlirredi  33754  mxidlirred  33755  drngmxidl  33759  drngmxidlr  33760  qsdrngilem  33776  dflringlem  33784  rsprprmprmidl  33812  rprmirredb  33822  1arithufdlem4  33837  selvply1rhmlem1  33910  selvply1rhmlem2  33911  selvply1rhmlem4  33913  selvply1rhmlem5  33914  selvply1rhm  33915  selvply1rhm0  33916  mvrvalind  33928  mplmulmvr  33929  evlextv  33932  psrmonmul  33940  esplyfval0  33954  esplyfvaln  33964  esplyind  33965  esplyindfv  33966  vietalem  33969  lsatdim  34007  drngdimgt0  34008  dimkerim  34017  evls1fldgencl  34060  algextdeglem1  34107  algextdeglem2  34108  algextdeglem3  34109  algextdeglem4  34110  algextdeglem5  34111  rtelextdg2  34117  constrextdg2lem  34138  constrext2chnlem  34140  constrfiss  34141  qtopt1  34225  locfinref  34231  zarcls0  34258  zarmxt1  34270  zarcmplem  34271  ordtrestNEW  34311  esumsnf  34454  esum2dlem  34482  rossros  34570  oms0  34687  carsggect  34708  eulerpartlems  34750  eulerpartlemgc  34752  eulerpartlemgh  34768  eulerpartlemgs2  34770  circlemeth  35027  hgt750lemb  35043  hgt750leme  35045  bnj1452  35440  pthhashvtx  35620  subfacp1lem1  35671  subfacp1lem5  35676  erdszelem4  35686  erdszelem8  35690  sconnpi1  35731  cvmscld  35765  cvmlift2lem6  35800  cvmlift2lem9  35803  cvmlift2lem11  35805  cvmlift2lem12  35806  mrsubvrs  36014  ellcsrspsn  36133  neibastop2lem  36891  topjoin  36896  fnejoin2  36900  weiunse  36999  pibt2  38083  lindsadd  38284  poimirlem3  38294  poimirlem9  38300  poimirlem28  38319  poimirlem32  38323  prdsbnd  38464  heiborlem8  38489  rrnequiv  38506  grpokerinj  38564  0idl  38696  prnc  38738  isfldidl  38739  lshpnel2N  39779  lsatfixedN  39803  lfl0f  39863  lkrlsp3  39898  elpaddatriN  40597  elpaddat  40598  elpadd2at  40600  pmodlem1  40640  osumcllem1N  40750  osumcllem2N  40751  osumcllem9N  40758  osumcllem10N  40759  pexmidlem6N  40769  pexmidlem7N  40770  dibss  41963  dochocsn  42175  dochsncom  42176  dochnel  42187  dihprrnlem1N  42218  dihprrnlem2  42219  djhlsmat  42221  dihsmsprn  42224  dvh4dimlem  42237  dvhdimlem  42238  dochsnnz  42244  dochsatshp  42245  dochsnshp  42247  dochexmid  42262  dochsnkr  42266  dochsnkr2cl  42268  dochfl1  42270  lcfl7lem  42293  lcfl6  42294  lcfl8  42296  lcfl9a  42299  lclkrlem2a  42301  lclkrlem2c  42303  lclkrlem2d  42304  lclkrlem2e  42305  lclkrlem2j  42310  lclkrlem2o  42315  lclkrlem2p  42316  lclkrlem2s  42319  lclkrlem2v  42322  lcfrlem14  42350  lcfrlem18  42354  lcfrlem19  42355  lcfrlem20  42356  lcfrlem23  42359  lcfrlem25  42361  lcdlkreqN  42416  mapdval4N  42426  mapdsn  42435  mapdhvmap  42563  hdmaprnlem4tN  42646  hdmapinvlem1  42712  hdmapinvlem2  42713  hdmapinvlem3  42714  hdmapinvlem4  42715  hdmapglem5  42716  hgmapvvlem3  42719  hdmapglem7a  42721  hdmapglem7b  42722  hdmapglem7  42723  hdmapoc  42725  aks6d1c5lem3  42924  deg1gprod  42927  sticksstones9  42941  sticksstones11  42943  rhmqusspan  42972  evlsbagval  43338  0prjspnrel  43379  elrfi  43445  cmpfiiin  43448  mzpcompact2lem  43502  dfac11  43809  pwssplit4  43836  rngunsnply  43916  flcidc  43917  proot1mul  43941  iocinico  43959  cantnfresb  44071  iunrelexp0  44448  frege81d  44493  k0004lem3  44895  mnuunid  45007  binomcxplemnn0  45079  islptre  46355  limciccioolb  46357  limcicciooub  46371  limcresiooub  46376  limcresioolb  46377  ioccncflimc  46619  icccncfext  46621  icocncflimc  46623  cncfiooicc  46628  dvnprodlem2  46681  dirkercncflem2  46838  dirkercncflem3  46839  fourierdlem48  46888  fourierdlem49  46889  fourierdlem79  46919  fourierdlem101  46941  sge0sup  47125  hoidmvlelem2  47330  hoiqssbl  47359  hspmbllem1  47360  hspmbllem2  47361  ovnovollem1  47390  fsumsplitsndif  48138  imaelsetpreimafv  48164  perfectALTVlem2  48507  stgrclnbgr0  48750  isubgr3stgrlem3  48753  1hegrlfgr  48917  gsumdifsndf  48966  sepfsepc  49726  discsubc  49862  iinfconstbas  49864