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 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-dif 3950  df-in 3954  df-ss 3964

This theorem is referenced by:  ssdif2d  4142  domunsncan  9096  fin1a2lem13  10435  seqcoll2  14458  rpnnen2lem11  16200  coprmprod  16631  mrieqv2d  17618  mrissmrid  17620  mreexexlem4d  17626  acsfiindd  18544  subdrgint  20690  lsppratlem3  21036  lsppratlem4  21037  f1lindf  21755  lpss3  23047  lpcls  23267  fin1aufil  23835  rrxmval  25332  rrxmetlem  25334  uniioombllem3  25513  i1fmul  25624  itg1addlem4  25627  itg1addlem4OLD  25628  itg1climres  25643  limciun  25822  ig1peu  26108  ig1pdvds  26113  fusgreghash2wspv  30144  pmtrcnel2  32813  pmtrcnelor  32814  tocyccntz  32865  elrspunidl  33144  elrspunsn  33145  indsumin  33641  sitgclg  33962  mthmpps  35192  poimirlem11  37104  poimirlem12  37105  poimirlem15  37108  dochfln0  40950  lcfl6  40973  lcfrlem16  41031  hdmaprnlem4N  41326  tfsconcatlem  42765  caragendifcl  45902