Theorem sscond 4069

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

Syntax hints:   → wi 4   ∖ cdif 3878   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-in 3888  df-ss 3898

This theorem is referenced by:  ssdif2d  4071  eldifeldifsn  4704  fin23lem26  9736  isercoll2  15017  fctop  21609  ntrss  21660  iunconnlem  22032  clsconn  22035  regr1lem  22344  blcld  23112  rrxdstprj1  24013  voliunlem1  24154  elrspunidl  31014  carsgclctunlem2  31687  salexct  42974  meaiininclem  43125  carageniuncllem2  43161