Theorem ssdifss 4090

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

Syntax hints:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

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 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-ss 3916

This theorem is referenced by:  ssdifssd  4097  xrsupss  13222  xrinfmss  13223  rpnnen2lem12  16148  lpval  23081  lpdifsn  23085  islp2  23087  lpcls  23306  mblfinlem3  37799  mblfinlem4  37800  voliunnfl  37804  redvmptabs  42557  ssdifcl  43754  sssymdifcl  43755  supxrmnf2  45619  infxrpnf2  45649  fourierdlem102  46394  fourierdlem114  46406  lindslinindimp2lem4  48649  lindslinindsimp2lem5  48650  lindslinindsimp2  48651  lincresunit3  48669