Theorem ssdifss 4102

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

Syntax hints:   → wi 4   ∖ cdif 3910   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-ss 3930

This theorem is referenced by:  ssdifssd  4109  xrsupss  13335  xrinfmss  13336  rpnnen2lem12  16281  lpval  23265  lpdifsn  23269  islp2  23271  lpcls  23490  mblfinlem3  38198  mblfinlem4  38199  voliunnfl  38203  redvmptabs  43011  ssdifcl  44189  sssymdifcl  44190  supxrmnf2  46039  infxrpnf2  46069  fourierdlem102  46814  fourierdlem114  46826  lindslinindimp2lem4  49126  lindslinindsimp2lem5  49127  lindslinindsimp2  49128  lincresunit3  49146