Theorem ssdifd 4092

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916

This theorem is used by:  ssdif2d  4095  domunsncan  9076  fin1a2lem13  10415  seqcoll2  14531  rpnnen2lem11  16313  coprmprod  16752  mrieqv2d  17728  mrissmrid  17730  mreexexlem4d  17736  acsfiindd  18642  chnind  18710  chnrev  18716  subdrgint  20970  lsppratlem3  21337  lsppratlem4  21338  f1lindf  22036  lpss3  23370  lpcls  23590  fin1aufil  24159  rrxmval  25634  rrxmetlem  25636  uniioombllem3  25814  i1fmul  25925  itg1addlem4  25928  itg1climres  25943  limciun  26122  ig1peu  26401  ig1pdvds  26406  fusgreghash2wspv  30816  indsumin  33308  pmtrcnel2  33531  pmtrcnelor  33532  tocyccntz  33585  elrspunidl  33857  elrspunsn  33858  sitgclg  34854  mthmpps  36162  poimirlem11  38381  poimirlem12  38382  poimirlem15  38385  dochfln0  42351  lcfl6  42374  lcfrlem16  42432  hdmaprnlem4N  42727  tfsconcatlem  44178  caragendifcl  47343