Theorem ssdifss 4149

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

Syntax hints:   → wi 4   ∖ cdif 3959   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-ss 3979

This theorem is referenced by:  ssdifssd  4156  xrsupss  13347  xrinfmss  13348  rpnnen2lem12  16257  lpval  23162  lpdifsn  23166  islp2  23168  lpcls  23387  mblfinlem3  37645  mblfinlem4  37646  voliunnfl  37650  redvmptabs  42368  ssdifcl  43560  sssymdifcl  43561  supxrmnf2  45382  infxrpnf2  45412  fourierdlem102  46163  fourierdlem114  46175  lindslinindimp2lem4  48306  lindslinindsimp2lem5  48307  lindslinindsimp2  48308  lincresunit3  48326