Theorem ssdifd 4145

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

Syntax hints:   → wi 4   ∖ cdif 3948   ⊆ wss 3951

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-dif 3954  df-ss 3968

This theorem is referenced by:  ssdif2d  4148  domunsncan  9112  fin1a2lem13  10452  seqcoll2  14504  rpnnen2lem11  16260  coprmprod  16698  mrieqv2d  17682  mrissmrid  17684  mreexexlem4d  17690  acsfiindd  18598  subdrgint  20804  lsppratlem3  21151  lsppratlem4  21152  f1lindf  21842  lpss3  23152  lpcls  23372  fin1aufil  23940  rrxmval  25439  rrxmetlem  25441  uniioombllem3  25620  i1fmul  25731  itg1addlem4  25734  itg1climres  25749  limciun  25929  ig1peu  26214  ig1pdvds  26219  fusgreghash2wspv  30354  indsumin  32847  chnind  33001  pmtrcnel2  33110  pmtrcnelor  33111  tocyccntz  33164  elrspunidl  33456  elrspunsn  33457  sitgclg  34344  mthmpps  35587  poimirlem11  37638  poimirlem12  37639  poimirlem15  37642  dochfln0  41479  lcfl6  41502  lcfrlem16  41560  hdmaprnlem4N  41855  tfsconcatlem  43349  caragendifcl  46529