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  23059  lpdifsn  23063  islp2  23065  lpcls  23284  mblfinlem3  37646  mblfinlem4  37647  voliunnfl  37651  redvmptabs  42341  ssdifcl  43553  sssymdifcl  43554  supxrmnf2  45422  infxrpnf2  45452  fourierdlem102  46199  fourierdlem114  46211  lindslinindimp2lem4  48443  lindslinindsimp2lem5  48444  lindslinindsimp2  48445  lincresunit3  48463