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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-ss 3916

This theorem is used by:  ssdifssd  4094  xrsupss  13362  xrinfmss  13363  rpnnen2lem12  16314  lpval  23365  lpdifsn  23369  islp2  23371  lpcls  23590  mblfinlem3  38409  mblfinlem4  38410  voliunnfl  38414  redvmptabs  43236  ssdifcl  44412  sssymdifcl  44413  supxrmnf2  46262  infxrpnf2  46292  fourierdlem102  47037  fourierdlem114  47049  lindslinindimp2lem4  49392  lindslinindsimp2lem5  49393  lindslinindsimp2  49394  lincresunit3  49412