Theorem ssdifd 4120

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

Syntax hints:   → wi 4   ∖ cdif 3923   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  ssdif2d  4123  domunsncan  9086  fin1a2lem13  10426  seqcoll2  14483  rpnnen2lem11  16242  coprmprod  16680  mrieqv2d  17651  mrissmrid  17653  mreexexlem4d  17659  acsfiindd  18563  subdrgint  20763  lsppratlem3  21110  lsppratlem4  21111  f1lindf  21782  lpss3  23082  lpcls  23302  fin1aufil  23870  rrxmval  25357  rrxmetlem  25359  uniioombllem3  25538  i1fmul  25649  itg1addlem4  25652  itg1climres  25667  limciun  25847  ig1peu  26132  ig1pdvds  26137  fusgreghash2wspv  30316  indsumin  32839  chnind  32991  pmtrcnel2  33101  pmtrcnelor  33102  tocyccntz  33155  elrspunidl  33443  elrspunsn  33444  sitgclg  34374  mthmpps  35604  poimirlem11  37655  poimirlem12  37656  poimirlem15  37659  dochfln0  41496  lcfl6  41519  lcfrlem16  41577  hdmaprnlem4N  41872  tfsconcatlem  43360  caragendifcl  46543