Theorem ssdifd 4099

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

Syntax hints:   → wi 4   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922

This theorem is referenced by:  ssdif2d  4102  domunsncan  9061  fin1a2lem13  10391  seqcoll2  14498  rpnnen2lem11  16275  coprmprod  16714  mrieqv2d  17690  mrissmrid  17692  mreexexlem4d  17698  acsfiindd  18604  chnind  18672  chnrev  18678  subdrgint  20906  lsppratlem3  21273  lsppratlem4  21274  f1lindf  21972  lpss3  23301  lpcls  23521  fin1aufil  24089  rrxmval  25564  rrxmetlem  25566  uniioombllem3  25744  i1fmul  25855  itg1addlem4  25858  itg1climres  25873  limciun  26053  ig1peu  26332  ig1pdvds  26337  fusgreghash2wspv  30686  indsumin  33181  pmtrcnel2  33410  pmtrcnelor  33411  tocyccntz  33464  elrspunidl  33736  elrspunsn  33737  sitgclg  34732  mthmpps  36074  poimirlem11  38282  poimirlem12  38283  poimirlem15  38286  dochfln0  42251  lcfl6  42274  lcfrlem16  42332  hdmaprnlem4N  42627  tfsconcatlem  44063  caragendifcl  47228