Theorem ssdifd 4105

Description: If 𝐴 is contained in 𝐵, then (𝐴 ∖ 𝐶) is contained in (𝐵 ∖ 𝐶). Deduction form of ssdif 4104. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
ssdifd	⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Proof of Theorem ssdifd

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		ssdif 4104	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3448  df-dif 3916  df-in 3920  df-ss 3930

This theorem is referenced by:  ssdif2d  4108  domunsncan  9023  fin1a2lem13  10357  seqcoll2  14376  rpnnen2lem11  16117  coprmprod  16548  mrieqv2d  17533  mrissmrid  17535  mreexexlem4d  17541  acsfiindd  18456  subdrgint  20326  lsppratlem3  20669  lsppratlem4  20670  f1lindf  21265  lpss3  22532  lpcls  22752  fin1aufil  23320  rrxmval  24806  rrxmetlem  24808  uniioombllem3  24986  i1fmul  25097  itg1addlem4  25100  itg1addlem4OLD  25101  itg1climres  25116  limciun  25295  ig1peu  25573  ig1pdvds  25578  fusgreghash2wspv  29342  pmtrcnel2  32011  pmtrcnelor  32012  tocyccntz  32063  elrspunidl  32279  indsumin  32710  sitgclg  33031  mthmpps  34263  poimirlem11  36162  poimirlem12  36163  poimirlem15  36166  dochfln0  40013  lcfl6  40036  lcfrlem16  40094  hdmaprnlem4N  40389  tfsconcatlem  41729  caragendifcl  44875