Theorem ssdifd 3944

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

Syntax hints:   → wi 4   ∖ cdif 3766   ⊆ wss 3769

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2777

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2786  df-cleq 2792  df-clel 2795  df-nfc 2930  df-v 3387  df-dif 3772  df-in 3776  df-ss 3783

This theorem is referenced by:  ssdif2d  3947  domunsncan  8302  fin1a2lem13  9522  seqcoll2  13498  rpnnen2lem11  15289  coprmprod  15709  mrieqv2d  16614  mrissmrid  16616  mreexexlem4d  16622  acsfiindd  17492  lsppratlem3  19472  lsppratlem4  19473  f1lindf  20486  lpss3  21277  lpcls  21497  fin1aufil  22064  rrxmval  23527  rrxmetlem  23529  uniioombllem3  23693  i1fmul  23804  itg1addlem4  23807  itg1climres  23822  limciun  23999  ig1peu  24272  ig1pdvds  24277  fusgreghash2wspv  27684  indsumin  30600  sitgclg  30920  mthmpps  31996  poimirlem11  33909  poimirlem12  33910  poimirlem15  33913  dochfln0  37498  lcfl6  37521  lcfrlem16  37579  hdmaprnlem4N  37874  caragendifcl  41474