Theorem ssdifd 4080

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896   ∖ cdif 4044

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-dif 4046

This theorem is used by:  ssdif2d  4083  domunsncan  9104  fin1a2lem13  10497  seqcoll2  14617  rpnnen2lem11  16401  coprmprod  16845  mrieqv2d  17822  mrissmrid  17824  mreexexlem4d  17830  acsfiindd  18736  chnind  18804  chnrev  18810  subdrgint  21069  lsppratlem3  21436  lsppratlem4  21437  f1lindf  22137  lpss3  23471  lpcls  23691  fin1aufil  24260  rrxmval  25735  rrxmetlem  25737  uniioombllem3  25915  i1fmul  26026  itg1addlem4  26029  itg1climres  26044  limciun  26223  ig1peu  26502  ig1pdvds  26507  fusgreghash2wspv  30945  indsumin  33478  pmtrcnel2  33701  pmtrcnelor  33702  tocyccntz  33755  elrspunidl  34028  elrspunsn  34029  sitgclg  35024  mthmpps  36465  poimirlem11  38686  poimirlem12  38687  poimirlem15  38690  dochfln0  42671  lcfl6  42694  lcfrlem16  42752  hdmaprnlem4N  43047  tfsconcatlem  44475  caragendifcl  47660