Theorem ssdifd 3779

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

Syntax hints:   → wi 4   ∖ cdif 3604   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-dif 3610  df-in 3614  df-ss 3621

This theorem is referenced by:  ssdif2d  3782  domunsncan  8101  fin1a2lem13  9272  seqcoll2  13287  rpnnen2lem11  14997  coprmprod  15422  mrieqv2d  16346  mrissmrid  16348  mreexexlem4d  16354  acsfiindd  17224  lsppratlem3  19197  lsppratlem4  19198  f1lindf  20209  lpss3  20996  lpcls  21216  fin1aufil  21783  rrxmval  23234  rrxmetlem  23236  uniioombllem3  23399  i1fmul  23508  itg1addlem4  23511  itg1climres  23526  limciun  23703  ig1peu  23976  ig1pdvds  23981  fusgreghash2wspv  27315  indsumin  30212  sitgclg  30532  mthmpps  31605  poimirlem11  33550  poimirlem12  33551  poimirlem15  33554  dochfln0  37083  lcfl6  37106  lcfrlem16  37164  hdmaprnlem4N  37462  caragendifcl  41049