Theorem ssdifss 4099

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

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

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 3446  df-dif 3914  df-ss 3928

This theorem is referenced by:  ssdifssd  4106  xrsupss  13245  xrinfmss  13246  rpnnen2lem12  16169  lpval  23002  lpdifsn  23006  islp2  23008  lpcls  23227  mblfinlem3  37626  mblfinlem4  37627  voliunnfl  37631  redvmptabs  42321  ssdifcl  43533  sssymdifcl  43534  supxrmnf2  45402  infxrpnf2  45432  fourierdlem102  46179  fourierdlem114  46191  lindslinindimp2lem4  48423  lindslinindsimp2lem5  48424  lindslinindsimp2  48425  lincresunit3  48443