Theorem ssdifssd 4122

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is also contained in 𝐵. Deduction form of ssdifss 4115. (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 4115	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3923   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  xpord3pred  8149  unblem1  9298  fin23lem26  10337  fin23lem29  10353  isf32lem8  10372  fprodfvdvdsd  16351  mrieqvlemd  17639  mrieqv2d  17649  mrissmrid  17651  mreexmrid  17653  mreexexlem2d  17655  mreexexlem4d  17657  acsfiindd  18561  ablfac1eulem  20053  c0rnghm  20493  cntzsdrg  20760  lbspss  21038  lspsolv  21102  lsppratlem3  21108  lsppratlem4  21109  lspprat  21112  islbs2  21113  islbs3  21114  lbsextlem2  21118  lbsextlem3  21119  lbsextlem4  21120  lpss3  23080  islp3  23082  neitr  23116  restlp  23119  lpcls  23300  qtoprest  23653  ufinffr  23865  cldsubg  24047  xrge0gsumle  24771  bcthlem5  25278  rrxmval  25355  cmmbl  25485  nulmbl2  25487  shftmbl  25489  iundisj2  25500  uniiccdif  25529  uniiccmbl  25541  itg1val2  25635  itg1cl  25636  itg1ge0  25637  i1fadd  25646  itg1addlem5  25651  i1fmulc  25654  itg1mulc  25655  itg10a  25661  itg1ge0a  25662  itg1climres  25665  mbfi1fseqlem4  25669  itgss3  25766  limcdif  25827  limcnlp  25829  limcmpt2  25835  perfdvf  25854  dvcnp2  25871  dvcnp2OLD  25872  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvferm1  25939  dvferm2  25941  ftc1lem6  25998  ig1peu  26130  ig1pdvds  26135  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmdvlem3  26361  rlimcnp  26925  wilthlem2  27029  newf  27814  elpwdifcl  32453  iundisj2f  32517  ofpreima2  32590  iundisj2fi  32720  tocyccntz  33101  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  0nellinds  33331  elrspunidl  33389  rprmdvdsprod  33495  ig1pmindeg  33557  lindsunlem  33610  lbsdiflsp0  33612  dimlssid  33618  fldextrspunlsp  33661  omsmeas  34301  eulerpartlemgs2  34358  ballotlemfrc  34505  hgt750lemd  34626  hgt750leme  34636  cvmscld  35241  unbdqndv1  36472  lindsadd  37583  lindsenlbs  37585  ftc1cnnc  37662  lsatfixedN  38973  dochsnkr  41437  hdmaprnlem4tN  41817  redvmptabs  42350  prjcrv0  42603  supminfxr2  45444  limcrecl  45606  cnrefiisplem  45806  fperdvper  45896  ismbl3  45963  ovolsplit  45965  ismbl4  45970  stoweidlem57  46034  dirkercncflem3  46082  fourierdlem42  46126  fourierdlem46  46129  fourierdlem62  46145  caragenuncllem  46489  caragendifcl  46491  omelesplit  46495  carageniuncllem2  46499  carageniuncl  46500  caragenel2d  46509  hspmbllem3  46605  hspmbl  46606  ovnsplit  46625  vonvolmbllem  46637  vonvolmbl  46638  lincdifsn  48348  lindslinindsimp1  48381  lincresunit3lem2  48404