Theorem ssdifd 4092

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

Syntax hints:   → wi 4   ∖ cdif 3894   ⊆ wss 3897

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 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-dif 3900  df-ss 3914

This theorem is referenced by:  ssdif2d  4095  domunsncan  8990  fin1a2lem13  10303  seqcoll2  14372  rpnnen2lem11  16133  coprmprod  16572  mrieqv2d  17545  mrissmrid  17547  mreexexlem4d  17553  acsfiindd  18459  chnind  18527  chnrev  18533  subdrgint  20718  lsppratlem3  21086  lsppratlem4  21087  f1lindf  21759  lpss3  23059  lpcls  23279  fin1aufil  23847  rrxmval  25332  rrxmetlem  25334  uniioombllem3  25513  i1fmul  25624  itg1addlem4  25627  itg1climres  25642  limciun  25822  ig1peu  26107  ig1pdvds  26112  fusgreghash2wspv  30315  indsumin  32843  pmtrcnel2  33059  pmtrcnelor  33060  tocyccntz  33113  elrspunidl  33393  elrspunsn  33394  sitgclg  34355  mthmpps  35626  poimirlem11  37681  poimirlem12  37682  poimirlem15  37685  dochfln0  41586  lcfl6  41609  lcfrlem16  41667  hdmaprnlem4N  41962  tfsconcatlem  43439  caragendifcl  46622