Theorem ssdifss 4087

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3896   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-ss 3916

This theorem is used by:  ssdifssd  4094  xrsupss  13439  xrinfmss  13440  rpnnen2lem12  16393  lpval  23457  lpdifsn  23461  islp2  23463  lpcls  23682  mblfinlem3  38577  mblfinlem4  38578  voliunnfl  38582  redvmptabs  43411  ssdifcl  44571  sssymdifcl  44572  supxrmnf2  46442  infxrpnf2  46472  fourierdlem102  47217  fourierdlem114  47229  lindslinindimp2lem4  49572  lindslinindsimp2lem5  49573  lindslinindsimp2  49574  lincresunit3  49592