Theorem ssdifss 4070

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

Syntax hints:   → wi 4   ∖ cdif 3880   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-dif 3886  df-ss 3900

This theorem is referenced by:  ssdifssd  4077  xrsupss  13252  xrinfmss  13253  rpnnen2lem12  16183  lpval  23122  lpdifsn  23126  islp2  23128  lpcls  23347  mblfinlem3  38026  mblfinlem4  38027  voliunnfl  38031  redvmptabs  42837  ssdifcl  44015  sssymdifcl  44016  supxrmnf2  45876  infxrpnf2  45906  fourierdlem102  46651  fourierdlem114  46663  lindslinindimp2lem4  48952  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  lincresunit3  48972