Theorem ssdifss 4078

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899   ∖ cdif 4047

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-dif 4049

This theorem is used by:  ssdifssd  4085  xrsupss  13449  xrinfmss  13450  rpnnen2lem12  16405  lpval  23469  lpdifsn  23473  islp2  23475  lpcls  23694  mblfinlem3  38717  mblfinlem4  38718  voliunnfl  38722  redvmptabs  43551  ssdifcl  44712  sssymdifcl  44713  supxrmnf2  46582  infxrpnf2  46612  fourierdlem102  47357  fourierdlem114  47369  lindslinindimp2lem4  49712  lindslinindsimp2lem5  49713  lindslinindsimp2  49714  lincresunit3  49732