Theorem ssdifd 4085

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

Syntax hints:   → wi 4   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  ssdif2d  4088  domunsncan  9015  fin1a2lem13  10334  seqcoll2  14427  rpnnen2lem11  16191  coprmprod  16630  mrieqv2d  17605  mrissmrid  17607  mreexexlem4d  17613  acsfiindd  18519  chnind  18587  chnrev  18593  subdrgint  20780  lsppratlem3  21147  lsppratlem4  21148  f1lindf  21802  lpss3  23109  lpcls  23329  fin1aufil  23897  rrxmval  25372  rrxmetlem  25374  uniioombllem3  25552  i1fmul  25663  itg1addlem4  25666  itg1climres  25681  limciun  25861  ig1peu  26140  ig1pdvds  26145  fusgreghash2wspv  30405  indsumin  32921  pmtrcnel2  33151  pmtrcnelor  33152  tocyccntz  33205  elrspunidl  33488  elrspunsn  33489  sitgclg  34486  mthmpps  35764  poimirlem11  37952  poimirlem12  37953  poimirlem15  37956  dochfln0  41923  lcfl6  41946  lcfrlem16  42004  hdmaprnlem4N  42299  tfsconcatlem  43764  caragendifcl  46942