Theorem snssd 4340

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	|- ( ph -> A e. B )

Assertion

Ref	Expression
snssd	|- ( ph -> { A } C_ B )

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 |- ( ph -> A e. B )
2		snssi 4339	. 2 |- ( A e. B -> { A } C_ B )
3	1, 2	syl 17	1 |- ( ph -> { A } C_ B )

Syntax hints:   -> wi 4   e. wcel 1990   C_ wss 3574   {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588  df-sn 4178

This theorem is referenced by:  sofld  5581  fsnex  6538  fr3nr  6979  wfrlem15  7429  oeeui  7682  ecinxp  7822  ralxpmap  7907  xpdom3  8058  domunsn  8110  mapdom3  8132  isinf  8173  ac6sfi  8204  pwfilem  8260  finsschain  8273  ssfii  8325  marypha1lem  8339  unxpwdom2  8493  en2other2  8832  fseqenlem1  8847  axdc3lem4  9275  axdc4lem  9277  ttukeylem7  9337  fpwwe2lem13  9464  canthwe  9473  canthp1lem1  9474  wuncval2  9569  un0addcl  11326  un0mulcl  11327  ssfzunsnext  12386  fseq1p1m1  12414  hashbclem  13236  hashf1lem1  13239  fsumge1  14529  incexclem  14568  isumltss  14580  rpnnen2lem11  14953  bitsinv1  15164  lcmfunsnlem2  15353  lcmfass  15359  phicl2  15473  vdwlem1  15685  vdwlem8  15692  vdwlem12  15696  vdwlem13  15697  0ram  15724  ramub1lem1  15730  ramub1lem2  15731  ramcl  15733  imasaddfnlem  16188  imasaddflem  16190  imasvscafn  16197  imasvscaf  16199  mrieqvlemd  16289  mreexmrid  16303  mreexexlem4d  16307  acsfiindd  17177  acsmapd  17178  gsumress  17276  gsumvallem2  17372  0subg  17619  cycsubg2cl  17632  pmtrprfv  17873  odf1o1  17987  gex1  18006  sylow2alem1  18032  sylow2alem2  18033  lsm01  18084  lsm02  18085  lsmdisj  18094  lsmdisj2  18095  prmcyg  18295  gsumzadd  18322  gsumconst  18334  gsumdifsnd  18360  gsumpt  18361  gsumxp  18375  dmdprdd  18398  dprdfadd  18419  dprdres  18427  dprdz  18429  dprdsn  18435  dprddisj2  18438  dprd2da  18441  dprd2d2  18443  dmdprdsplit2lem  18444  dpjcntz  18451  dpjdisj  18452  dpjlsm  18453  dpjidcl  18457  ablfacrp  18465  ablfac1eu  18472  pgpfac1lem1  18473  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfac1lem5  18478  pgpfaclem2  18481  kerf1hrm  18743  lsssn0  18948  lss0ss  18949  lsptpcl  18979  lspsnvsi  19004  lspun0  19011  pwssplit1  19059  lsmpr  19089  lsppr  19093  lspsntri  19097  lspsolvlem  19142  lspsolv  19143  lsppratlem1  19147  lsppratlem3  19149  lsppratlem4  19150  islbs3  19155  lbsextlem4  19161  rsp1  19224  lidlnz  19228  lidldvgen  19255  psrlidm  19403  psrridm  19404  mplmonmul  19464  mulgrhm2  19847  zndvds  19898  mdetdiaglem  20404  mdetrlin  20408  mdetrsca  20409  mdetrsca2  20410  mdetrlin2  20413  mdetunilem5  20422  mdetunilem9  20426  mdetmul  20429  en2top  20789  rest0  20973  ordtrest  21006  iscnp4  21067  cnconst2  21087  cnpdis  21097  ist1-2  21151  cnt1  21154  dishaus  21186  discmp  21201  cmpcld  21205  conncompid  21234  dis2ndc  21263  dislly  21300  dissnref  21331  comppfsc  21335  llycmpkgen2  21353  cmpkgen  21354  1stckgenlem  21356  1stckgen  21357  ptbasfi  21384  txdis  21435  txdis1cn  21438  txcmplem1  21444  xkohaus  21456  xkoptsub  21457  xkoinjcn  21490  snfbas  21670  trnei  21696  isufil2  21712  ufileu  21723  filufint  21724  uffixsn  21729  ufildom1  21730  flimopn  21779  hausflim  21785  flimcf  21786  flimclslem  21788  flimsncls  21790  cnpflf2  21804  cnpflf  21805  fclsneii  21821  fclsfnflim  21831  fcfnei  21839  flfcntr  21847  alexsubALTlem3  21853  alexsubALTlem4  21854  ptcmplem2  21857  cldsubg  21914  snclseqg  21919  qustgphaus  21926  tsmsgsum  21942  tsmsid  21943  tgptsmscld  21954  tsmsxplem1  21956  tsmsxplem2  21957  ust0  22023  ustuqtop1  22045  neipcfilu  22100  prdsdsf  22172  prdsxmetlem  22173  prdsmet  22175  imasdsf1olem  22178  xpsdsval  22186  prdsbl  22296  prdsxmslem2  22334  idnghm  22547  icccmplem2  22626  metnrmlem2  22663  ioombl  23333  volivth  23375  itg11  23458  i1fmulclem  23469  itg2mulclem  23513  itgsplitioo  23604  limcvallem  23635  limcdif  23640  ellimc2  23641  limcflf  23645  limcmpt2  23648  limcres  23650  cnplimc  23651  limccnp  23655  limccnp2  23656  limcco  23657  dvreslem  23673  dvaddbr  23701  dvmulbr  23702  dvcmulf  23708  dvef  23743  dvivth  23773  lhop2  23778  lhop  23779  ply1remlem  23922  fta1blem  23928  ig1peu  23931  ig1pdvds  23936  plyco0  23948  elply2  23952  plyf  23954  elplyr  23957  elplyd  23958  ply1term  23960  ply0  23964  plyeq0lem  23966  plyeq0  23967  plypf1  23968  plyaddlem  23971  plymullem  23972  dgrlem  23985  coef2  23987  coeidlem  23993  plyco  23997  coemulhi  24010  plycj  24033  vieta1  24067  taylf  24115  radcnv0  24170  abelth  24195  rlimcnp  24692  xrlimcnp  24695  amgm  24717  wilthlem2  24795  basellem7  24813  basellem9  24815  ppiprm  24877  chtprm  24879  musumsum  24918  muinv  24919  logexprlim  24950  perfectlem2  24955  dchrhash  24996  rpvmasum2  25201  axlowdimlem7  25828  axlowdimlem10  25831  upgrex  25987  upgr1elem  26007  uvtxanm1nbgr  26305  umgr2v2e  26421  0oo  27644  sh0le  28299  disjiunel  29409  fprodeq02  29569  qtopt1  29902  locfinref  29908  ordtrestNEW  29967  esumsnf  30126  esum2dlem  30154  rossros  30243  oms0  30359  carsggect  30380  eulerpartlems  30422  eulerpartlemgc  30424  eulerpartlemgh  30440  eulerpartlemgs2  30442  plymulx0  30624  circlemeth  30718  hgt750lemb  30734  hgt750leme  30736  bnj1452  31120  subfacp1lem1  31161  subfacp1lem5  31166  erdszelem4  31176  erdszelem8  31180  sconnpi1  31221  cvmscld  31255  cvmlift2lem6  31290  cvmlift2lem9  31293  cvmlift2lem11  31295  cvmlift2lem12  31296  mrsubvrs  31419  slerec  31923  neibastop2lem  32355  topjoin  32360  fnejoin2  32364  poimirlem3  33412  poimirlem9  33418  poimirlem28  33437  poimirlem32  33441  prdsbnd  33592  heiborlem8  33617  rrnequiv  33634  grpokerinj  33692  0idl  33824  prnc  33866  isfldidl  33867  lshpnel2N  34272  lsatfixedN  34296  lfl0f  34356  lkrlsp3  34391  elpaddatriN  35089  elpaddat  35090  elpadd2at  35092  pmodlem1  35132  osumcllem1N  35242  osumcllem2N  35243  osumcllem9N  35250  osumcllem10N  35251  pexmidlem6N  35261  pexmidlem7N  35262  dibss  36458  dochocsn  36670  dochsncom  36671  dochnel  36682  dihprrnlem1N  36713  dihprrnlem2  36714  djhlsmat  36716  dihsmsprn  36719  dvh4dimlem  36732  dvhdimlem  36733  dochsnnz  36739  dochsatshp  36740  dochsnshp  36742  dochexmid  36757  dochsnkr  36761  dochsnkr2cl  36763  dochfl1  36765  lcfl7lem  36788  lcfl6  36789  lcfl8  36791  lcfl9a  36794  lclkrlem2a  36796  lclkrlem2c  36798  lclkrlem2d  36799  lclkrlem2e  36800  lclkrlem2j  36805  lclkrlem2o  36810  lclkrlem2p  36811  lclkrlem2s  36814  lclkrlem2v  36817  lcfrlem14  36845  lcfrlem18  36849  lcfrlem19  36850  lcfrlem20  36851  lcfrlem23  36854  lcfrlem25  36856  lcdlkreqN  36911  mapdval4N  36921  mapdsn  36930  mapdhvmap  37058  hdmaprnlem4tN  37144  hdmapinvlem1  37210  hdmapinvlem2  37211  hdmapinvlem3  37212  hdmapinvlem4  37213  hdmapglem5  37214  hgmapvvlem3  37217  hdmapglem7a  37219  hdmapglem7b  37220  hdmapglem7  37221  hdmapoc  37223  elrfi  37257  cmpfiiin  37260  mzpcompact2lem  37314  dfac11  37632  pwssplit4  37659  rngunsnply  37743  flcidc  37744  acsfn1p  37769  proot1mul  37777  iocinico  37797  iunrelexp0  37994  frege81d  38039  k0004lem3  38447  binomcxplemnn0  38548  fsumsplit1  39804  islptre  39851  limciccioolb  39853  limcicciooub  39869  limcresiooub  39874  limcresioolb  39875  ioccncflimc  40098  icccncfext  40100  icocncflimc  40102  cncfiooicc  40107  dvnprodlem2  40162  dirkercncflem2  40321  dirkercncflem3  40322  fourierdlem48  40371  fourierdlem49  40372  fourierdlem79  40402  fourierdlem101  40424  sge0sup  40608  hoidmvlelem2  40810  hoiqssbl  40839  hspmbllem1  40840  hspmbllem2  40841  ovnovollem1  40870  fsumsplitsndif  41343  perfectALTVlem2  41631  1hegrlfgr  41713  gsumdifsndf  42144