Theorem ssdifd 4141

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

Syntax hints:   → wi 4   ∖ cdif 3946   ⊆ wss 3949

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966

This theorem is referenced by:  ssdif2d  4144  domunsncan  9072  fin1a2lem13  10407  seqcoll2  14426  rpnnen2lem11  16167  coprmprod  16598  mrieqv2d  17583  mrissmrid  17585  mreexexlem4d  17591  acsfiindd  18506  subdrgint  20419  lsppratlem3  20762  lsppratlem4  20763  f1lindf  21377  lpss3  22648  lpcls  22868  fin1aufil  23436  rrxmval  24922  rrxmetlem  24924  uniioombllem3  25102  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  itg1climres  25232  limciun  25411  ig1peu  25689  ig1pdvds  25694  fusgreghash2wspv  29588  pmtrcnel2  32251  pmtrcnelor  32252  tocyccntz  32303  elrspunidl  32546  elrspunsn  32547  indsumin  33020  sitgclg  33341  mthmpps  34573  poimirlem11  36499  poimirlem12  36500  poimirlem15  36503  dochfln0  40348  lcfl6  40371  lcfrlem16  40429  hdmaprnlem4N  40724  tfsconcatlem  42086  caragendifcl  45230