Theorem ssdifss 4094

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

Syntax hints:   → wi 4   ∖ cdif 3902   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-dif 3908  df-ss 3922

This theorem is referenced by:  ssdifssd  4101  xrsupss  13330  xrinfmss  13331  rpnnen2lem12  16276  lpval  23296  lpdifsn  23300  islp2  23302  lpcls  23521  mblfinlem3  38330  mblfinlem4  38331  voliunnfl  38335  redvmptabs  43141  ssdifcl  44317  sssymdifcl  44318  supxrmnf2  46167  infxrpnf2  46197  fourierdlem102  46942  fourierdlem114  46954  lindslinindimp2lem4  49261  lindslinindsimp2lem5  49262  lindslinindsimp2  49263  lincresunit3  49281