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 17	1 ⊢ (𝜑 → (𝐴 ∖ 𝐶) ⊆ (𝐵 ∖ 𝐶))

Syntax hints:   → wi 4   ∖ cdif 3900   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-ss 3920

This theorem is referenced by:  ssdif2d  4102  domunsncan  9017  fin1a2lem13  10334  seqcoll2  14400  rpnnen2lem11  16161  coprmprod  16600  mrieqv2d  17574  mrissmrid  17576  mreexexlem4d  17582  acsfiindd  18488  chnind  18556  chnrev  18562  subdrgint  20748  lsppratlem3  21116  lsppratlem4  21117  f1lindf  21789  lpss3  23100  lpcls  23320  fin1aufil  23888  rrxmval  25373  rrxmetlem  25375  uniioombllem3  25554  i1fmul  25665  itg1addlem4  25668  itg1climres  25683  limciun  25863  ig1peu  26148  ig1pdvds  26153  fusgreghash2wspv  30422  indsumin  32954  pmtrcnel2  33184  pmtrcnelor  33185  tocyccntz  33238  elrspunidl  33521  elrspunsn  33522  sitgclg  34520  mthmpps  35798  poimirlem11  37882  poimirlem12  37883  poimirlem15  37886  dochfln0  41853  lcfl6  41876  lcfrlem16  41934  hdmaprnlem4N  42229  tfsconcatlem  43693  caragendifcl  46872