Theorem snssd 4281

Description: The singleton of an element of a class is a subset of the class (deduction rule). (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 4280	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ∈ wcel 1977   ⊆ wss 3540  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554  df-sn 4126

This theorem is referenced by:  sofld  5500  fsnex  6438  fr3nr  6871  wfrlem15  7316  oeeui  7569  ecinxp  7709  ralxpmap  7793  xpdom3  7943  domunsn  7995  mapdom3  8017  isinf  8058  ac6sfi  8089  pwfilem  8143  finsschain  8156  ssfii  8208  marypha1lem  8222  unxpwdom2  8376  en2other2  8715  fseqenlem1  8730  axdc3lem4  9158  axdc4lem  9160  ttukeylem7  9220  fpwwe2lem13  9343  canthwe  9352  canthp1lem1  9353  wuncval2  9448  un0addcl  11203  un0mulcl  11204  ssfzunsn  12257  fseq1p1m1  12283  hashbclem  13093  hashf1lem1  13096  fsumge1  14370  incexclem  14407  isumltss  14419  rpnnen2lem11  14792  bitsinv1  15002  lcmfunsnlem2  15191  lcmfass  15197  phicl2  15311  vdwlem1  15523  vdwlem8  15530  vdwlem12  15534  vdwlem13  15535  0ram  15562  ramub1lem1  15568  ramub1lem2  15569  ramcl  15571  imasaddfnlem  16011  imasaddflem  16013  imasvscafn  16020  imasvscaf  16022  mrieqvlemd  16112  mreexmrid  16126  mreexexlem4d  16130  acsfiindd  17000  acsmapd  17001  gsumress  17099  gsumvallem2  17195  0subg  17442  cycsubg2cl  17455  pmtrprfv  17696  odf1o1  17810  gex1  17829  sylow2alem1  17855  sylow2alem2  17856  lsm01  17907  lsm02  17908  lsmdisj  17917  lsmdisj2  17918  prmcyg  18118  gsumzadd  18145  gsumconst  18157  gsumdifsnd  18183  gsumpt  18184  gsumxp  18198  dmdprdd  18221  dprdfadd  18242  dprdres  18250  dprdz  18252  dprdsn  18258  dprddisj2  18261  dprd2da  18264  dprd2d2  18266  dmdprdsplit2lem  18267  dpjcntz  18274  dpjdisj  18275  dpjlsm  18276  dpjidcl  18280  ablfacrp  18288  ablfac1eu  18295  pgpfac1lem1  18296  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfac1lem5  18301  pgpfaclem2  18304  kerf1hrm  18566  lsssn0  18769  lss0ss  18770  lsptpcl  18800  lspsnvsi  18825  lspun0  18832  pwssplit1  18880  lsmpr  18910  lsppr  18914  lspsntri  18918  lspsolvlem  18963  lspsolv  18964  lsppratlem1  18968  lsppratlem3  18970  lsppratlem4  18971  islbs3  18976  lbsextlem4  18982  rsp1  19045  lidlnz  19049  lidldvgen  19076  psrlidm  19224  psrridm  19225  mplmonmul  19285  mulgrhm2  19666  zndvds  19717  mdetdiaglem  20223  mdetrlin  20227  mdetrsca  20228  mdetrsca2  20229  mdetrlin2  20232  mdetunilem5  20241  mdetunilem9  20245  mdetmul  20248  en2top  20600  rest0  20783  ordtrest  20816  iscnp4  20877  cnconst2  20897  cnpdis  20907  ist1-2  20961  cnt1  20964  dishaus  20996  discmp  21011  cmpcld  21015  concompid  21044  dis2ndc  21073  dislly  21110  dissnref  21141  comppfsc  21145  llycmpkgen2  21163  cmpkgen  21164  1stckgenlem  21166  1stckgen  21167  ptbasfi  21194  txdis  21245  txdis1cn  21248  txcmplem1  21254  xkohaus  21266  xkoptsub  21267  xkoinjcn  21300  snfbas  21480  trnei  21506  isufil2  21522  ufileu  21533  filufint  21534  uffixsn  21539  ufildom1  21540  flimopn  21589  hausflim  21595  flimcf  21596  flimclslem  21598  flimsncls  21600  cnpflf2  21614  cnpflf  21615  fclsneii  21631  fclsfnflim  21641  fcfnei  21649  flfcntr  21657  alexsubALTlem3  21663  alexsubALTlem4  21664  ptcmplem2  21667  cldsubg  21724  snclseqg  21729  qustgphaus  21736  tsmsgsum  21752  tsmsid  21753  tgptsmscld  21764  tsmsxplem1  21766  tsmsxplem2  21767  ust0  21833  ustuqtop1  21855  neipcfilu  21910  prdsdsf  21982  prdsxmetlem  21983  prdsmet  21985  imasdsf1olem  21988  xpsdsval  21996  prdsbl  22106  prdsxmslem2  22144  idnghm  22357  icccmplem2  22434  metnrmlem2  22471  ioombl  23140  volivth  23181  itg11  23264  i1fmulclem  23275  itg2mulclem  23319  itgsplitioo  23410  limcvallem  23441  limcdif  23446  ellimc2  23447  limcflf  23451  limcmpt2  23454  limcres  23456  cnplimc  23457  limccnp  23461  limccnp2  23462  limcco  23463  dvreslem  23479  dvaddbr  23507  dvmulbr  23508  dvcmulf  23514  dvef  23547  dvivth  23577  lhop2  23582  lhop  23583  ply1remlem  23726  fta1blem  23732  ig1peu  23735  ig1pdvds  23740  plyco0  23752  elply2  23756  plyf  23758  elplyr  23761  elplyd  23762  ply1term  23764  ply0  23768  plyeq0lem  23770  plyeq0  23771  plypf1  23772  plyaddlem  23775  plymullem  23776  dgrlem  23789  coef2  23791  coeidlem  23797  plyco  23801  coemulhi  23814  plycj  23837  vieta1  23871  taylf  23919  radcnv0  23974  abelth  23999  rlimcnp  24492  xrlimcnp  24495  amgm  24517  wilthlem2  24595  basellem7  24613  basellem9  24615  ppiprm  24677  chtprm  24679  musumsum  24718  muinv  24719  logexprlim  24750  perfectlem2  24755  dchrhash  24796  rpvmasum2  25001  axlowdimlem7  25628  axlowdimlem10  25631  upgrex  25759  upgr1elem  25778  umgraex  25852  umgra1  25855  uslgra1  25901  usgra1  25902  uvtxnm1nbgra  26022  constr1trl  26118  eupa0  26501  eupap1  26503  0oo  27028  sh0le  27683  disjiunel  28791  qtopt1  29230  locfinref  29236  ordtrestNEW  29295  esumsnf  29453  esum2dlem  29481  rossros  29570  oms0  29686  carsggect  29707  eulerpartlems  29749  eulerpartlemgc  29751  eulerpartlemgh  29767  eulerpartlemgs2  29769  plymulx0  29950  bnj1452  30374  subfacp1lem1  30415  subfacp1lem5  30420  erdszelem4  30430  erdszelem8  30434  sconpi1  30475  cvmscld  30509  cvmlift2lem6  30544  cvmlift2lem9  30547  cvmlift2lem11  30549  cvmlift2lem12  30550  mrsubvrs  30673  neibastop2lem  31525  topjoin  31530  fnejoin2  31534  poimirlem3  32582  poimirlem9  32588  poimirlem28  32607  poimirlem32  32611  prdsbnd  32762  heiborlem8  32787  rrnequiv  32804  grpokerinj  32862  0idl  32994  prnc  33036  isfldidl  33037  lshpnel2N  33290  lsatfixedN  33314  lfl0f  33374  lkrlsp3  33409  elpaddatriN  34107  elpaddat  34108  elpadd2at  34110  pmodlem1  34150  osumcllem1N  34260  osumcllem2N  34261  osumcllem9N  34268  osumcllem10N  34269  pexmidlem6N  34279  pexmidlem7N  34280  dibss  35476  dochocsn  35688  dochsncom  35689  dochnel  35700  dihprrnlem1N  35731  dihprrnlem2  35732  djhlsmat  35734  dihsmsprn  35737  dvh4dimlem  35750  dvhdimlem  35751  dochsnnz  35757  dochsatshp  35758  dochsnshp  35760  dochexmid  35775  dochsnkr  35779  dochsnkr2cl  35781  dochfl1  35783  lcfl7lem  35806  lcfl6  35807  lcfl8  35809  lcfl9a  35812  lclkrlem2a  35814  lclkrlem2c  35816  lclkrlem2d  35817  lclkrlem2e  35818  lclkrlem2j  35823  lclkrlem2o  35828  lclkrlem2p  35829  lclkrlem2s  35832  lclkrlem2v  35835  lcfrlem14  35863  lcfrlem18  35867  lcfrlem19  35868  lcfrlem20  35869  lcfrlem23  35872  lcfrlem25  35874  lcdlkreqN  35929  mapdval4N  35939  mapdsn  35948  mapdhvmap  36076  hdmaprnlem4tN  36162  hdmapinvlem1  36228  hdmapinvlem2  36229  hdmapinvlem3  36230  hdmapinvlem4  36231  hdmapglem5  36232  hgmapvvlem3  36235  hdmapglem7a  36237  hdmapglem7b  36238  hdmapglem7  36239  hdmapoc  36241  elrfi  36275  cmpfiiin  36278  mzpcompact2lem  36332  dfac11  36650  pwssplit4  36677  rngunsnply  36762  flcidc  36763  acsfn1p  36788  proot1mul  36796  iocinico  36816  iunrelexp0  37013  frege81d  37058  k0004lem3  37467  binomcxplemnn0  37570  fsumsplit1  38639  islptre  38686  limciccioolb  38688  limcicciooub  38704  limcresiooub  38709  limcresioolb  38710  ioccncflimc  38771  icccncfext  38773  icocncflimc  38775  cncfiooicc  38780  dvnprodlem2  38837  dirkercncflem2  38997  dirkercncflem3  38998  fourierdlem48  39047  fourierdlem49  39048  fourierdlem79  39078  fourierdlem101  39100  sge0sup  39284  hoidmvlelem2  39486  hoiqssbl  39515  hspmbllem1  39516  hspmbllem2  39517  ovnovollem1  39546  perfectALTVlem2  40165  fsumsplitsndif  40372  uvtxanm1nbgr  40631  1hegrlfgr  40722  umgr2v2e  40741  gsumdifsndf  41937