Theorem ssdifd 4098

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

Syntax hints:   → wi 4   ∖ cdif 3901   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921

This theorem is referenced by:  ssdif2d  4101  domunsncan  9049  fin1a2lem13  10369  seqcoll2  14478  rpnnen2lem11  16256  coprmprod  16695  mrieqv2d  17671  mrissmrid  17673  mreexexlem4d  17679  acsfiindd  18585  chnind  18653  chnrev  18659  subdrgint  20852  lsppratlem3  21219  lsppratlem4  21220  f1lindf  21874  lpss3  23204  lpcls  23424  fin1aufil  23992  rrxmval  25467  rrxmetlem  25469  uniioombllem3  25647  i1fmul  25758  itg1addlem4  25761  itg1climres  25776  limciun  25956  ig1peu  26235  ig1pdvds  26240  fusgreghash2wspv  30537  indsumin  33039  pmtrcnel2  33270  pmtrcnelor  33271  tocyccntz  33324  elrspunidl  33614  elrspunsn  33615  sitgclg  34639  mthmpps  35932  poimirlem11  38130  poimirlem12  38131  poimirlem15  38134  dochfln0  42101  lcfl6  42124  lcfrlem16  42182  hdmaprnlem4N  42477  tfsconcatlem  43913  caragendifcl  47088