Theorem ssdifd 4104

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

Syntax hints:   → wi 4   ∖ cdif 3908   ⊆ wss 3911

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  ssdif2d  4107  domunsncan  9018  fin1a2lem13  10341  seqcoll2  14406  rpnnen2lem11  16168  coprmprod  16607  mrieqv2d  17580  mrissmrid  17582  mreexexlem4d  17588  acsfiindd  18494  subdrgint  20723  lsppratlem3  21091  lsppratlem4  21092  f1lindf  21764  lpss3  23064  lpcls  23284  fin1aufil  23852  rrxmval  25338  rrxmetlem  25340  uniioombllem3  25519  i1fmul  25630  itg1addlem4  25633  itg1climres  25648  limciun  25828  ig1peu  26113  ig1pdvds  26118  fusgreghash2wspv  30314  indsumin  32835  chnind  32983  pmtrcnel2  33062  pmtrcnelor  33063  tocyccntz  33116  elrspunidl  33392  elrspunsn  33393  sitgclg  34326  mthmpps  35562  poimirlem11  37618  poimirlem12  37619  poimirlem15  37622  dochfln0  41464  lcfl6  41487  lcfrlem16  41545  hdmaprnlem4N  41840  tfsconcatlem  43318  caragendifcl  46505