Theorem ssdifss 4115

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

Syntax hints:   → wi 4   ∖ cdif 3936   ⊆ wss 3939

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-dif 3942  df-in 3946  df-ss 3955

This theorem is referenced by:  ssdifssd  4122  xrsupss  12705  xrinfmss  12706  rpnnen2lem12  15581  lpval  21750  lpdifsn  21754  islp2  21756  lpcls  21975  mblfinlem3  34935  mblfinlem4  34936  voliunnfl  34940  ssdifcl  39936  sssymdifcl  39937  supxrmnf2  41713  infxrpnf2  41745  fourierdlem102  42500  fourierdlem114  42512  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  lincresunit3  44543