Theorem ssdifss 4106

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 4102	. 2 ⊢ (𝐴 ∖ 𝐶) ⊆ 𝐴
2		sstr 3958	. 2 ⊢ (((𝐴 ∖ 𝐶) ⊆ 𝐴 ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∖ 𝐶) ⊆ 𝐵)
3	1, 2	mpan 690	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∖ 𝐶) ⊆ 𝐵)

Syntax hints:   → wi 4   ∖ cdif 3914   ⊆ wss 3917

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 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-ss 3934

This theorem is referenced by:  ssdifssd  4113  xrsupss  13276  xrinfmss  13277  rpnnen2lem12  16200  lpval  23033  lpdifsn  23037  islp2  23039  lpcls  23258  mblfinlem3  37660  mblfinlem4  37661  voliunnfl  37665  redvmptabs  42355  ssdifcl  43567  sssymdifcl  43568  supxrmnf2  45436  infxrpnf2  45466  fourierdlem102  46213  fourierdlem114  46225  lindslinindimp2lem4  48454  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  lincresunit3  48474