Theorem ssdifss 3703

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

Syntax hints:   → wi 4   ∖ cdif 3537   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554

This theorem is referenced by:  ssdifssd  3710  xrsupss  12011  xrinfmss  12012  rpnnen2lem12  14793  lpval  20753  lpdifsn  20757  islp2  20759  lpcls  20978  mblfinlem3  32618  mblfinlem4  32619  voliunnfl  32623  ssdifcl  36895  sssymdifcl  36896  fourierdlem102  39101  fourierdlem114  39113  lindslinindimp2lem4  42044  lindslinindsimp2lem5  42045  lindslinindsimp2  42046  lincresunit3  42064