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  9064  fin1a2lem13  10395  seqcoll2  14501  rpnnen2lem11  16279  coprmprod  16718  mrieqv2d  17694  mrissmrid  17696  mreexexlem4d  17702  acsfiindd  18608  chnind  18676  chnrev  18682  subdrgint  20883  lsppratlem3  21250  lsppratlem4  21251  f1lindf  21940  lpss3  23269  lpcls  23489  fin1aufil  24057  rrxmval  25532  rrxmetlem  25534  uniioombllem3  25712  i1fmul  25823  itg1addlem4  25826  itg1climres  25841  limciun  26021  ig1peu  26300  ig1pdvds  26305  fusgreghash2wspv  30626  indsumin  33121  pmtrcnel2  33350  pmtrcnelor  33351  tocyccntz  33404  elrspunidl  33679  elrspunsn  33680  sitgclg  34676  mthmpps  35972  poimirlem11  38169  poimirlem12  38170  poimirlem15  38173  dochfln0  42140  lcfl6  42163  lcfrlem16  42221  hdmaprnlem4N  42516  tfsconcatlem  43954  caragendifcl  47119