Theorem ssdifss 4163

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

Syntax hints:   → wi 4   ∖ cdif 3973   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-ss 3993

This theorem is referenced by:  ssdifssd  4170  xrsupss  13371  xrinfmss  13372  rpnnen2lem12  16273  lpval  23168  lpdifsn  23172  islp2  23174  lpcls  23393  mblfinlem3  37619  mblfinlem4  37620  voliunnfl  37624  ssdifcl  43533  sssymdifcl  43534  supxrmnf2  45348  infxrpnf2  45378  fourierdlem102  46129  fourierdlem114  46141  lindslinindimp2lem4  48190  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  lincresunit3  48210