Theorem ssdifssd 3641

Description: If is contained in , then is also contained in . Deduction form of ssdifss 3634. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1

Assertion

Ref	Expression
ssdifssd

Proof of Theorem ssdifssd

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2
2		ssdifss 3634	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  \cdif 3472  C_wss 3475

This theorem is referenced by:  unblem1  7792  fin23lem26  8726  fin23lem29  8742  isf32lem8  8761  mrieqvlemd  15026  mrieqv2d  15036  mrissmrid  15038  mreexmrid  15040  mreexexlem2d  15042  mreexexlem4d  15044  acsfiindd  15807  ablfac1eulem  17123  lbspss  17728  lspsolv  17789  lsppratlem3  17795  lsppratlem4  17796  lspprat  17799  islbs2  17800  islbs3  17801  lbsextlem2  17805  lbsextlem3  17806  lbsextlem4  17807  lpss3  19645  islp3  19647  neitr  19681  restlp  19684  lpcls  19865  qtoprest  20218  ufinffr  20430  cldsubg  20609  xrge0gsumle  21338  bcthlem5  21767  rrxmval  21832  cmmbl  21945  nulmbl2  21947  shftmbl  21949  iundisj2  21959  uniiccdif  21987  uniiccmbl  21999  itg1val2  22091  itg1cl  22092  itg1ge0  22093  i1fadd  22102  itg1addlem5  22107  i1fmulc  22110  itg1mulc  22111  itg10a  22117  itg1ge0a  22118  itg1climres  22121  mbfi1fseqlem4  22125  itgss3  22221  limcdif  22280  limcnlp  22282  limcmpt2  22288  perfdvf  22307  dvcnp2  22323  dvaddbr  22341  dvmulbr  22342  dvferm1  22386  dvferm2  22388  ftc1lem6  22442  ig1peu  22572  ig1pdvds  22577  taylthlem1  22768  taylthlem2  22769  ulmdvlem3  22797  rlimcnp  23295  wilthlem2  23343  iundisj2f  27449  ofpreima2  27508  iundisj2fi  27602  eulerpartlemgs2  28319  ballotlemfrc  28465  cvmscld  28718  ftc1cnnc  30089  cntzsdrg  31151  limcrecl  31635  fperdvper  31715  stoweidlem57  31839  dirkercncflem3  31887  fourierdlem42  31931  fourierdlem46  31935  fourierdlem62  31951  c0rnghm  32719  lincdifsn  33025  lindslinindsimp1  33058  lincresunit3lem2  33081  lsatfixedN  34734  dochsnkr  37199  hdmaprnlem4tN  37582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-dif 3478  df-in 3482  df-ss 3489