Theorem sscond 4095

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

Syntax hints:   → wi 4   ∖ cdif 3895   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-dif 3901  df-ss 3915

This theorem is referenced by:  ssdif2d  4097  eldifeldifsn  4764  fin23lem26  10227  isercoll2  15583  fctop  22939  ntrss  22990  iunconnlem  23362  clsconn  23365  regr1lem  23674  blcld  24440  rrxdstprj1  25356  voliunlem1  25498  elrgspnsubrunlem2  33258  elrspunidl  33437  carsgclctunlem2  34404  salexct  46494  meaiininclem  46646  carageniuncllem2  46682  seposep  49087