Theorem ssdifd 4139

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

Syntax hints:   → wi 4   ∖ cdif 3944   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  ssdif2d  4142  domunsncan  9074  fin1a2lem13  10409  seqcoll2  14430  rpnnen2lem11  16171  coprmprod  16602  mrieqv2d  17587  mrissmrid  17589  mreexexlem4d  17595  acsfiindd  18510  subdrgint  20562  lsppratlem3  20907  lsppratlem4  20908  f1lindf  21596  lpss3  22868  lpcls  23088  fin1aufil  23656  rrxmval  25153  rrxmetlem  25155  uniioombllem3  25334  i1fmul  25445  itg1addlem4  25448  itg1addlem4OLD  25449  itg1climres  25464  limciun  25643  ig1peu  25924  ig1pdvds  25929  fusgreghash2wspv  29855  pmtrcnel2  32521  pmtrcnelor  32522  tocyccntz  32573  elrspunidl  32820  elrspunsn  32821  indsumin  33318  sitgclg  33639  mthmpps  34871  poimirlem11  36802  poimirlem12  36803  poimirlem15  36806  dochfln0  40651  lcfl6  40674  lcfrlem16  40732  hdmaprnlem4N  41027  tfsconcatlem  42388  caragendifcl  45528