Metamath Proof Explorer

Theorem difss

Description: Subclass relationship for class difference. Exercise 14 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)

Ref Expression
Assertion difss ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴

Proof

Step Hyp Ref Expression
1 eldifi ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑥 ∈ 𝐴 )
2 1 ssriv ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴