Theorem ssdifss 4115

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

Syntax hints:   → wi 4   ∖ cdif 3923   ⊆ wss 3926

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-dif 3929  df-ss 3943

This theorem is referenced by:  ssdifssd  4122  xrsupss  13325  xrinfmss  13326  rpnnen2lem12  16243  lpval  23077  lpdifsn  23081  islp2  23083  lpcls  23302  mblfinlem3  37683  mblfinlem4  37684  voliunnfl  37688  redvmptabs  42403  ssdifcl  43595  sssymdifcl  43596  supxrmnf2  45460  infxrpnf2  45490  fourierdlem102  46237  fourierdlem114  46249  lindslinindimp2lem4  48437  lindslinindsimp2lem5  48438  lindslinindsimp2  48439  lincresunit3  48457