Theorem ssdifss 4081

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

Syntax hints:   → wi 4   ∖ cdif 3887   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-dif 3893  df-ss 3907

This theorem is referenced by:  ssdifssd  4088  xrsupss  13255  xrinfmss  13256  rpnnen2lem12  16186  lpval  23117  lpdifsn  23121  islp2  23123  lpcls  23342  mblfinlem3  37997  mblfinlem4  37998  voliunnfl  38002  redvmptabs  42809  ssdifcl  44019  sssymdifcl  44020  supxrmnf2  45882  infxrpnf2  45912  fourierdlem102  46657  fourierdlem114  46669  lindslinindimp2lem4  48952  lindslinindsimp2lem5  48953  lindslinindsimp2  48954  lincresunit3  48972