Theorem ssdifss 4079

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900   ∖ cdif 4048

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-dif 4050

This theorem is used by:  ssdifssd  4086  xrsupss  13479  xrinfmss  13480  rpnnen2lem12  16437  lpval  23512  lpdifsn  23516  islp2  23518  lpcls  23737  zzedom  33958  mblfinlem3  38845  mblfinlem4  38846  voliunnfl  38850  redvmptabs  43677  ssdifcl  44833  sssymdifcl  44834  supxrmnf2  46716  infxrpnf2  46746  fourierdlem102  47491  fourierdlem114  47503  lindslinindimp2lem4  49904  lindslinindsimp2lem5  49905  lindslinindsimp2  49906  lincresunit3  49924