Theorem ssdifd 4096

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

Syntax hints:   → wi 4   ∖ cdif 3900   ⊆ wss 3903

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-dif 3906  df-ss 3920

This theorem is referenced by:  ssdif2d  4099  domunsncan  8994  fin1a2lem13  10306  seqcoll2  14372  rpnnen2lem11  16133  coprmprod  16572  mrieqv2d  17545  mrissmrid  17547  mreexexlem4d  17553  acsfiindd  18459  subdrgint  20688  lsppratlem3  21056  lsppratlem4  21057  f1lindf  21729  lpss3  23029  lpcls  23249  fin1aufil  23817  rrxmval  25303  rrxmetlem  25305  uniioombllem3  25484  i1fmul  25595  itg1addlem4  25598  itg1climres  25613  limciun  25793  ig1peu  26078  ig1pdvds  26083  fusgreghash2wspv  30279  indsumin  32805  chnind  32953  pmtrcnel2  33032  pmtrcnelor  33033  tocyccntz  33086  elrspunidl  33365  elrspunsn  33366  sitgclg  34310  mthmpps  35559  poimirlem11  37615  poimirlem12  37616  poimirlem15  37619  dochfln0  41460  lcfl6  41483  lcfrlem16  41541  hdmaprnlem4N  41836  tfsconcatlem  43313  caragendifcl  46499