Theorem ssdifd 4099

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  ssdif2d  4102  domunsncan  9072  fin1a2lem13  10411  seqcoll2  14522  rpnnen2lem11  16304  coprmprod  16743  mrieqv2d  17719  mrissmrid  17721  mreexexlem4d  17727  acsfiindd  18633  chnind  18701  chnrev  18707  subdrgint  20958  lsppratlem3  21325  lsppratlem4  21326  f1lindf  22024  lpss3  23353  lpcls  23573  fin1aufil  24142  rrxmval  25617  rrxmetlem  25619  uniioombllem3  25797  i1fmul  25908  itg1addlem4  25911  itg1climres  25926  limciun  26106  ig1peu  26385  ig1pdvds  26390  fusgreghash2wspv  30759  indsumin  33253  pmtrcnel2  33476  pmtrcnelor  33477  tocyccntz  33530  elrspunidl  33802  elrspunsn  33803  sitgclg  34799  mthmpps  36113  poimirlem11  38341  poimirlem12  38342  poimirlem15  38345  dochfln0  42311  lcfl6  42334  lcfrlem16  42392  hdmaprnlem4N  42687  tfsconcatlem  44123  caragendifcl  47288