Theorem ssdifss 4132

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

Syntax hints:   → wi 4   ∖ cdif 3941   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-v 3463  df-dif 3947  df-ss 3961

This theorem is referenced by:  ssdifssd  4139  xrsupss  13328  xrinfmss  13329  rpnnen2lem12  16210  lpval  23092  lpdifsn  23096  islp2  23098  lpcls  23317  mblfinlem3  37265  mblfinlem4  37266  voliunnfl  37270  ssdifcl  43145  sssymdifcl  43146  supxrmnf2  44955  infxrpnf2  44985  fourierdlem102  45736  fourierdlem114  45748  lindslinindimp2lem4  47717  lindslinindsimp2lem5  47718  lindslinindsimp2  47719  lincresunit3  47737