Theorem ssdifd 4119

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

Syntax hints:   → wi 4   ∖ cdif 3935   ⊆ wss 3938

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954

This theorem is referenced by:  ssdif2d  4122  domunsncan  8619  fin1a2lem13  9836  seqcoll2  13826  rpnnen2lem11  15579  coprmprod  16007  mrieqv2d  16912  mrissmrid  16914  mreexexlem4d  16920  acsfiindd  17789  subdrgint  19584  lsppratlem3  19923  lsppratlem4  19924  f1lindf  20968  lpss3  21754  lpcls  21974  fin1aufil  22542  rrxmval  24010  rrxmetlem  24012  uniioombllem3  24188  i1fmul  24299  itg1addlem4  24302  itg1climres  24317  limciun  24494  ig1peu  24767  ig1pdvds  24772  fusgreghash2wspv  28116  pmtrcnel2  30736  pmtrcnelor  30737  tocyccntz  30788  indsumin  31283  sitgclg  31602  mthmpps  32831  poimirlem11  34905  poimirlem12  34906  poimirlem15  34909  dochfln0  38615  lcfl6  38638  lcfrlem16  38696  hdmaprnlem4N  38991  caragendifcl  42803