Theorem ssdifd 4107

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

Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  ssdif2d  4110  domunsncan  9065  fin1a2lem13  10396  seqcoll2  14502  rpnnen2lem11  16280  coprmprod  16719  mrieqv2d  17695  mrissmrid  17697  mreexexlem4d  17703  acsfiindd  18609  chnind  18677  chnrev  18683  subdrgint  20884  lsppratlem3  21251  lsppratlem4  21252  f1lindf  21941  lpss3  23270  lpcls  23490  fin1aufil  24058  rrxmval  25533  rrxmetlem  25535  uniioombllem3  25713  i1fmul  25824  itg1addlem4  25827  itg1climres  25842  limciun  26022  ig1peu  26301  ig1pdvds  26306  fusgreghash2wspv  30627  indsumin  33122  pmtrcnel2  33351  pmtrcnelor  33352  tocyccntz  33405  elrspunidl  33680  elrspunsn  33681  sitgclg  34677  mthmpps  35973  poimirlem11  38170  poimirlem12  38171  poimirlem15  38174  dochfln0  42141  lcfl6  42164  lcfrlem16  42222  hdmaprnlem4N  42517  tfsconcatlem  43955  caragendifcl  47120