Theorem ssdifss 4093

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

Syntax hints:   → wi 4   ∖ cdif 3901   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-dif 3907  df-ss 3921

This theorem is referenced by:  ssdifssd  4100  xrsupss  13307  xrinfmss  13308  rpnnen2lem12  16238  lpval  23177  lpdifsn  23181  islp2  23183  lpcls  23402  mblfinlem3  38111  mblfinlem4  38112  voliunnfl  38116  redvmptabs  42922  ssdifcl  44100  sssymdifcl  44101  supxrmnf2  45960  infxrpnf2  45990  fourierdlem102  46735  fourierdlem114  46747  lindslinindimp2lem4  49036  lindslinindsimp2lem5  49037  lindslinindsimp2  49038  lincresunit3  49056