Theorem ssdifd 4068

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

Syntax hints:   → wi 4   ∖ cdif 3878   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898

This theorem is referenced by:  ssdif2d  4071  domunsncan  8600  fin1a2lem13  9823  seqcoll2  13819  rpnnen2lem11  15569  coprmprod  15995  mrieqv2d  16902  mrissmrid  16904  mreexexlem4d  16910  acsfiindd  17779  subdrgint  19575  lsppratlem3  19914  lsppratlem4  19915  f1lindf  20511  lpss3  21749  lpcls  21969  fin1aufil  22537  rrxmval  24009  rrxmetlem  24011  uniioombllem3  24189  i1fmul  24300  itg1addlem4  24303  itg1climres  24318  limciun  24497  ig1peu  24772  ig1pdvds  24777  fusgreghash2wspv  28120  pmtrcnel2  30784  pmtrcnelor  30785  tocyccntz  30836  elrspunidl  31014  indsumin  31391  sitgclg  31710  mthmpps  32942  poimirlem11  35068  poimirlem12  35069  poimirlem15  35072  dochfln0  38773  lcfl6  38796  lcfrlem16  38854  hdmaprnlem4N  39149  caragendifcl  43153