Theorem sscond 4099

Description: If 𝐴 is contained in 𝐵, then (𝐶 ∖ 𝐵) is contained in (𝐶 ∖ 𝐴). Deduction form of sscon 4096. (Contributed by David Moews, 1-May-2017.)

Hypothesis

Ref	Expression
ssdifd.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)

Assertion

Ref	Expression
sscond	⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))

Proof of Theorem sscond

Step	Hyp	Ref	Expression
1		ssdifd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sscon 4096	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 ∖ 𝐵) ⊆ (𝐶 ∖ 𝐴))

Syntax hints:   → wi 4   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-dif 3908  df-ss 3922

This theorem is referenced by:  ssdif2d  4101  eldifeldifsn  4765  fin23lem26  10238  isercoll2  15594  fctop  22907  ntrss  22958  iunconnlem  23330  clsconn  23333  regr1lem  23642  blcld  24409  rrxdstprj1  25325  voliunlem1  25467  elrgspnsubrunlem2  33201  elrspunidl  33378  carsgclctunlem2  34289  salexct  46319  meaiininclem  46471  carageniuncllem2  46507  seposep  48914