Theorem ssdifd 4108

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

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

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 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  ssdif2d  4111  domunsncan  9041  fin1a2lem13  10365  seqcoll2  14430  rpnnen2lem11  16192  coprmprod  16631  mrieqv2d  17600  mrissmrid  17602  mreexexlem4d  17608  acsfiindd  18512  subdrgint  20712  lsppratlem3  21059  lsppratlem4  21060  f1lindf  21731  lpss3  23031  lpcls  23251  fin1aufil  23819  rrxmval  25305  rrxmetlem  25307  uniioombllem3  25486  i1fmul  25597  itg1addlem4  25600  itg1climres  25615  limciun  25795  ig1peu  26080  ig1pdvds  26085  fusgreghash2wspv  30264  indsumin  32785  chnind  32937  pmtrcnel2  33047  pmtrcnelor  33048  tocyccntz  33101  elrspunidl  33399  elrspunsn  33400  sitgclg  34333  mthmpps  35569  poimirlem11  37625  poimirlem12  37626  poimirlem15  37629  dochfln0  41471  lcfl6  41494  lcfrlem16  41552  hdmaprnlem4N  41847  tfsconcatlem  43325  caragendifcl  46512