Theorem ssdifd 4075

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

Syntax hints:   → wi 4   ∖ cdif 3884   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-in 3894  df-ss 3904

This theorem is referenced by:  ssdif2d  4078  domunsncan  8859  fin1a2lem13  10168  seqcoll2  14179  rpnnen2lem11  15933  coprmprod  16366  mrieqv2d  17348  mrissmrid  17350  mreexexlem4d  17356  acsfiindd  18271  subdrgint  20071  lsppratlem3  20411  lsppratlem4  20412  f1lindf  21029  lpss3  22295  lpcls  22515  fin1aufil  23083  rrxmval  24569  rrxmetlem  24571  uniioombllem3  24749  i1fmul  24860  itg1addlem4  24863  itg1addlem4OLD  24864  itg1climres  24879  limciun  25058  ig1peu  25336  ig1pdvds  25341  fusgreghash2wspv  28699  pmtrcnel2  31359  pmtrcnelor  31360  tocyccntz  31411  elrspunidl  31606  indsumin  31990  sitgclg  32309  mthmpps  33544  poimirlem11  35788  poimirlem12  35789  poimirlem15  35792  dochfln0  39491  lcfl6  39514  lcfrlem16  39572  hdmaprnlem4N  39867  caragendifcl  44052