Theorem ssdifd 4104

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

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

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 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  ssdif2d  4107  domunsncan  9018  fin1a2lem13  10341  seqcoll2  14406  rpnnen2lem11  16168  coprmprod  16607  mrieqv2d  17576  mrissmrid  17578  mreexexlem4d  17584  acsfiindd  18488  subdrgint  20688  lsppratlem3  21035  lsppratlem4  21036  f1lindf  21707  lpss3  23007  lpcls  23227  fin1aufil  23795  rrxmval  25281  rrxmetlem  25283  uniioombllem3  25462  i1fmul  25573  itg1addlem4  25576  itg1climres  25591  limciun  25771  ig1peu  26056  ig1pdvds  26061  fusgreghash2wspv  30237  indsumin  32758  chnind  32910  pmtrcnel2  33020  pmtrcnelor  33021  tocyccntz  33074  elrspunidl  33372  elrspunsn  33373  sitgclg  34306  mthmpps  35542  poimirlem11  37598  poimirlem12  37599  poimirlem15  37602  dochfln0  41444  lcfl6  41467  lcfrlem16  41525  hdmaprnlem4N  41820  tfsconcatlem  43298  caragendifcl  46485