Theorem ssdifss 4114

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

Syntax hints:   → wi 4   ∖ cdif 3935   ⊆ wss 3938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-dif 3941  df-in 3945  df-ss 3954

This theorem is referenced by:  ssdifssd  4121  xrsupss  12705  xrinfmss  12706  rpnnen2lem12  15580  lpval  21749  lpdifsn  21753  islp2  21755  lpcls  21974  mblfinlem3  34933  mblfinlem4  34934  voliunnfl  34938  ssdifcl  39937  sssymdifcl  39938  supxrmnf2  41714  infxrpnf2  41746  fourierdlem102  42500  fourierdlem114  42512  lindslinindimp2lem4  44523  lindslinindsimp2lem5  44524  lindslinindsimp2  44525  lincresunit3  44543