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 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-ss 3921

This theorem is referenced by:  ssdifssd  4100  xrsupss  13312  xrinfmss  13313  rpnnen2lem12  16257  lpval  23199  lpdifsn  23203  islp2  23205  lpcls  23424  mblfinlem3  38158  mblfinlem4  38159  voliunnfl  38163  redvmptabs  42969  ssdifcl  44147  sssymdifcl  44148  supxrmnf2  46007  infxrpnf2  46037  fourierdlem102  46782  fourierdlem114  46794  lindslinindimp2lem4  49083  lindslinindsimp2lem5  49084  lindslinindsimp2  49085  lincresunit3  49103