Theorem ssdifss 4094

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

This proof depends on syntax axioms:   → wi 4   ∖ cdif 3903   ⊆ wss 3906

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-dif 3909  df-ss 3923

This theorem is used by:  ssdifssd  4101  xrsupss  13353  xrinfmss  13354  rpnnen2lem12  16305  lpval  23348  lpdifsn  23352  islp2  23354  lpcls  23573  mblfinlem3  38369  mblfinlem4  38370  voliunnfl  38374  redvmptabs  43181  ssdifcl  44357  sssymdifcl  44358  supxrmnf2  46207  infxrpnf2  46237  fourierdlem102  46982  fourierdlem114  46994  lindslinindimp2lem4  49300  lindslinindsimp2lem5  49301  lindslinindsimp2  49302  lincresunit3  49320