Theorem ssdifd 4111

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

Syntax hints:   → wi 4   ∖ cdif 3914   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  ssdif2d  4114  domunsncan  9046  fin1a2lem13  10372  seqcoll2  14437  rpnnen2lem11  16199  coprmprod  16638  mrieqv2d  17607  mrissmrid  17609  mreexexlem4d  17615  acsfiindd  18519  subdrgint  20719  lsppratlem3  21066  lsppratlem4  21067  f1lindf  21738  lpss3  23038  lpcls  23258  fin1aufil  23826  rrxmval  25312  rrxmetlem  25314  uniioombllem3  25493  i1fmul  25604  itg1addlem4  25607  itg1climres  25622  limciun  25802  ig1peu  26087  ig1pdvds  26092  fusgreghash2wspv  30271  indsumin  32792  chnind  32944  pmtrcnel2  33054  pmtrcnelor  33055  tocyccntz  33108  elrspunidl  33406  elrspunsn  33407  sitgclg  34340  mthmpps  35576  poimirlem11  37632  poimirlem12  37633  poimirlem15  37636  dochfln0  41478  lcfl6  41501  lcfrlem16  41559  hdmaprnlem4N  41854  tfsconcatlem  43332  caragendifcl  46519