Theorem ssdifss 4073

Description: Preservation of a subclass relationship by class difference. (Contributed by NM, 15-Feb-2007.)

Assertion

Ref	Expression
ssdifss	⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Proof of Theorem ssdifss

Step	Hyp	Ref	Expression
1		difss 4069	. 2 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴
2		sstr 3931	. 2 ⊢ (((𝐴 ∖ 𝐶) ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∖ 𝐶) ⊆ 𝐵)
3	1, 2	mpan 686	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1540  df-ex 1778  df-sb 2063  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3436  df-dif 3892  df-in 3896  df-ss 3906

This theorem is referenced by:  ssdifssd  4080  xrsupss  13071  xrinfmss  13072  rpnnen2lem12  15962  lpval  22318  lpdifsn  22322  islp2  22324  lpcls  22543  mblfinlem3  35844  mblfinlem4  35845  voliunnfl  35849  ssdifcl  41202  sssymdifcl  41203  supxrmnf2  43007  infxrpnf2  43037  fourierdlem102  43784  fourierdlem114  43796  lindslinindimp2lem4  45842  lindslinindsimp2lem5  45843  lindslinindsimp2  45844  lincresunit3  45862