Theorem ssdifss 3741

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

Syntax hints:   → wi 4   ∖ cdif 3571   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588

This theorem is referenced by:  ssdifssd  3748  xrsupss  12139  xrinfmss  12140  rpnnen2lem12  14954  lpval  20943  lpdifsn  20947  islp2  20949  lpcls  21168  mblfinlem3  33448  mblfinlem4  33449  voliunnfl  33453  ssdifcl  37876  sssymdifcl  37877  supxrmnf2  39660  infxrpnf2  39693  fourierdlem102  40425  fourierdlem114  40437  lindslinindimp2lem4  42250  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lincresunit3  42270