Theorem ssdifd 4071

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-in 3890  df-ss 3900

This theorem is referenced by:  ssdif2d  4074  domunsncan  8812  fin1a2lem13  10099  seqcoll2  14107  rpnnen2lem11  15861  coprmprod  16294  mrieqv2d  17265  mrissmrid  17267  mreexexlem4d  17273  acsfiindd  18186  subdrgint  19986  lsppratlem3  20326  lsppratlem4  20327  f1lindf  20939  lpss3  22203  lpcls  22423  fin1aufil  22991  rrxmval  24474  rrxmetlem  24476  uniioombllem3  24654  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  itg1climres  24784  limciun  24963  ig1peu  25241  ig1pdvds  25246  fusgreghash2wspv  28600  pmtrcnel2  31261  pmtrcnelor  31262  tocyccntz  31313  elrspunidl  31508  indsumin  31890  sitgclg  32209  mthmpps  33444  poimirlem11  35715  poimirlem12  35716  poimirlem15  35719  dochfln0  39418  lcfl6  39441  lcfrlem16  39499  hdmaprnlem4N  39794  caragendifcl  43942