Theorem ssdifss 4080

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

Syntax hints:   → wi 4   ∖ cdif 3886   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906

This theorem is referenced by:  ssdifssd  4087  xrsupss  13261  xrinfmss  13262  rpnnen2lem12  16192  lpval  23104  lpdifsn  23108  islp2  23110  lpcls  23329  mblfinlem3  37980  mblfinlem4  37981  voliunnfl  37985  redvmptabs  42792  ssdifcl  43998  sssymdifcl  43999  supxrmnf2  45861  infxrpnf2  45891  fourierdlem102  46636  fourierdlem114  46648  lindslinindimp2lem4  48937  lindslinindsimp2lem5  48938  lindslinindsimp2  48939  lincresunit3  48957