Theorem ssdifd 4097

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  ssdif2d  4100  domunsncan  9005  fin1a2lem13  10322  seqcoll2  14388  rpnnen2lem11  16149  coprmprod  16588  mrieqv2d  17562  mrissmrid  17564  mreexexlem4d  17570  acsfiindd  18476  chnind  18544  chnrev  18550  subdrgint  20736  lsppratlem3  21104  lsppratlem4  21105  f1lindf  21777  lpss3  23088  lpcls  23308  fin1aufil  23876  rrxmval  25361  rrxmetlem  25363  uniioombllem3  25542  i1fmul  25653  itg1addlem4  25656  itg1climres  25671  limciun  25851  ig1peu  26136  ig1pdvds  26141  fusgreghash2wspv  30410  indsumin  32943  pmtrcnel2  33172  pmtrcnelor  33173  tocyccntz  33226  elrspunidl  33509  elrspunsn  33510  sitgclg  34499  mthmpps  35776  poimirlem11  37832  poimirlem12  37833  poimirlem15  37836  dochfln0  41747  lcfl6  41770  lcfrlem16  41828  hdmaprnlem4N  42123  tfsconcatlem  43588  caragendifcl  46768