Theorem ssdifss 4092

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-ss 3918

This theorem is referenced by:  ssdifssd  4099  xrsupss  13224  xrinfmss  13225  rpnnen2lem12  16150  lpval  23083  lpdifsn  23087  islp2  23089  lpcls  23308  mblfinlem3  37860  mblfinlem4  37861  voliunnfl  37865  redvmptabs  42625  ssdifcl  43822  sssymdifcl  43823  supxrmnf2  45687  infxrpnf2  45717  fourierdlem102  46462  fourierdlem114  46474  lindslinindimp2lem4  48717  lindslinindsimp2lem5  48718  lindslinindsimp2  48719  lincresunit3  48737