Theorem ssdifd 4095

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

Syntax hints:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916

This theorem is referenced by:  ssdif2d  4098  domunsncan  9003  fin1a2lem13  10320  seqcoll2  14386  rpnnen2lem11  16147  coprmprod  16586  mrieqv2d  17560  mrissmrid  17562  mreexexlem4d  17568  acsfiindd  18474  chnind  18542  chnrev  18548  subdrgint  20734  lsppratlem3  21102  lsppratlem4  21103  f1lindf  21775  lpss3  23086  lpcls  23306  fin1aufil  23874  rrxmval  25359  rrxmetlem  25361  uniioombllem3  25540  i1fmul  25651  itg1addlem4  25654  itg1climres  25669  limciun  25849  ig1peu  26134  ig1pdvds  26139  fusgreghash2wspv  30359  indsumin  32892  pmtrcnel2  33121  pmtrcnelor  33122  tocyccntz  33175  elrspunidl  33458  elrspunsn  33459  sitgclg  34448  mthmpps  35725  poimirlem11  37771  poimirlem12  37772  poimirlem15  37775  dochfln0  41676  lcfl6  41699  lcfrlem16  41757  hdmaprnlem4N  42052  tfsconcatlem  43520  caragendifcl  46700