Theorem ssdifd 4154

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

Syntax hints:   → wi 4   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  ssdif2d  4157  domunsncan  9110  fin1a2lem13  10449  seqcoll2  14500  rpnnen2lem11  16256  coprmprod  16694  mrieqv2d  17683  mrissmrid  17685  mreexexlem4d  17691  acsfiindd  18610  subdrgint  20820  lsppratlem3  21168  lsppratlem4  21169  f1lindf  21859  lpss3  23167  lpcls  23387  fin1aufil  23955  rrxmval  25452  rrxmetlem  25454  uniioombllem3  25633  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  itg1climres  25763  limciun  25943  ig1peu  26228  ig1pdvds  26233  fusgreghash2wspv  30363  chnind  32984  pmtrcnel2  33092  pmtrcnelor  33093  tocyccntz  33146  elrspunidl  33435  elrspunsn  33436  indsumin  34002  sitgclg  34323  mthmpps  35566  poimirlem11  37617  poimirlem12  37618  poimirlem15  37621  dochfln0  41459  lcfl6  41482  lcfrlem16  41540  hdmaprnlem4N  41835  tfsconcatlem  43325  caragendifcl  46469