Theorem ssdifss 4091

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

Syntax hints:   → wi 4   ∖ cdif 3900   ⊆ wss 3903

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 3438  df-dif 3906  df-ss 3920

This theorem is referenced by:  ssdifssd  4098  xrsupss  13211  xrinfmss  13212  rpnnen2lem12  16134  lpval  23024  lpdifsn  23028  islp2  23030  lpcls  23249  mblfinlem3  37643  mblfinlem4  37644  voliunnfl  37648  redvmptabs  42337  ssdifcl  43548  sssymdifcl  43549  supxrmnf2  45416  infxrpnf2  45446  fourierdlem102  46193  fourierdlem114  46205  lindslinindimp2lem4  48450  lindslinindsimp2lem5  48451  lindslinindsimp2  48452  lincresunit3  48470