Theorem ssdifssd 4101

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  xpord3pred  8155  unblem1  9260  fin23lem26  10325  fin23lem29  10341  isf32lem8  10360  fprodfvdvdsd  16419  mrieqvlemd  17712  mrieqv2d  17722  mrissmrid  17724  mreexmrid  17726  mreexexlem2d  17728  mreexexlem4d  17730  acsfiindd  18636  ablfac1eulem  20193  c0rnghm  20689  cntzsdrg  20960  lbspss  21258  lspsolv  21322  lsppratlem3  21328  lsppratlem4  21329  lspprat  21332  islbs2  21333  islbs3  21334  lbsextlem2  21338  lbsextlem3  21339  lbsextlem4  21340  lpss3  23356  islp3  23358  neitr  23392  restlp  23395  lpcls  23576  qtoprest  23930  ufinffr  24142  cldsubg  24324  xrge0gsumle  25047  bcthlem5  25543  rrxmval  25620  cmmbl  25749  nulmbl2  25751  shftmbl  25753  iundisj2  25764  uniiccdif  25793  uniiccmbl  25805  itg1val2  25899  itg1cl  25900  itg1ge0  25901  i1fadd  25910  itg1addlem5  25915  i1fmulc  25918  itg1mulc  25919  itg10a  25925  itg1ge0a  25926  itg1climres  25929  mbfi1fseqlem4  25933  itgss3  26030  limcdif  26091  limcnlp  26093  limcmpt2  26099  perfdvf  26118  dvcnp2  26135  dvaddbr  26153  dvmulbr  26154  dvferm1  26200  dvferm2  26202  ftc1lem6  26256  ig1peu  26388  ig1pdvds  26393  taylthlem1  26592  taylthlem2  26593  ulmdvlem3  26621  rlimcnp  27186  wilthlem2  27289  newf  28087  elpwdifcl  32948  iundisj2f  33011  ofpreima2  33087  iundisj2fi  33217  tocyccntz  33533  fxpsdrg  33564  elrgspnsubrunlem1  33636  elrgspnsubrunlem2  33637  0nellinds  33754  elrspunidl  33805  rprmdvdsprod  33893  ig1pmindeg  33961  lindsunlem  34083  lbsdiflsp0  34085  dimlssid  34091  fldextrspunlsp  34133  omsmeas  34783  eulerpartlemgs2  34840  ballotlemfrc  34987  hgt750lemd  35105  hgt750leme  35115  cvmscld  35807  unbdqndv1  37159  lindsadd  38326  lindsenlbs  38328  ftc1cnnc  38405  lsatfixedN  39846  dochsnkr  42309  hdmaprnlem4tN  42689  redvmptabs  43199  prjcrv0  43443  supminfxr2  46261  limcrecl  46423  cnrefiisplem  46621  fperdvper  46711  ismbl3  46778  ovolsplit  46780  ismbl4  46785  stoweidlem57  46849  dirkercncflem3  46897  fourierdlem42  46941  fourierdlem46  46944  fourierdlem62  46960  caragenuncllem  47304  caragendifcl  47306  omelesplit  47310  carageniuncllem2  47314  carageniuncl  47315  caragenel2d  47324  hspmbllem3  47420  hspmbl  47421  ovnsplit  47440  vonvolmbllem  47452  vonvolmbl  47453  lincdifsn  49281  lindslinindsimp1  49314  lincresunit3lem2  49337