Theorem ssdifss 4103

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

Syntax hints:   → wi 4   ∖ cdif 3911   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-ss 3931

This theorem is referenced by:  ssdifssd  4110  xrsupss  13269  xrinfmss  13270  rpnnen2lem12  16193  lpval  23026  lpdifsn  23030  islp2  23032  lpcls  23251  mblfinlem3  37653  mblfinlem4  37654  voliunnfl  37658  redvmptabs  42348  ssdifcl  43560  sssymdifcl  43561  supxrmnf2  45429  infxrpnf2  45459  fourierdlem102  46206  fourierdlem114  46218  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lincresunit3  48470