Theorem ssdifd 4086

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  ssdif2d  4089  domunsncan  9009  fin1a2lem13  10328  seqcoll2  14421  rpnnen2lem11  16185  coprmprod  16624  mrieqv2d  17599  mrissmrid  17601  mreexexlem4d  17607  acsfiindd  18513  chnind  18581  chnrev  18587  subdrgint  20774  lsppratlem3  21142  lsppratlem4  21143  f1lindf  21815  lpss3  23122  lpcls  23342  fin1aufil  23910  rrxmval  25385  rrxmetlem  25387  uniioombllem3  25565  i1fmul  25676  itg1addlem4  25679  itg1climres  25694  limciun  25874  ig1peu  26153  ig1pdvds  26158  fusgreghash2wspv  30423  indsumin  32939  pmtrcnel2  33169  pmtrcnelor  33170  tocyccntz  33223  elrspunidl  33506  elrspunsn  33507  sitgclg  34505  mthmpps  35783  poimirlem11  37969  poimirlem12  37970  poimirlem15  37973  dochfln0  41940  lcfl6  41963  lcfrlem16  42021  hdmaprnlem4N  42316  tfsconcatlem  43785  caragendifcl  46963