Description: Subclass relationship for class difference. Exercise 14 of TakeutiZaring p. 22. (Contributed by NM, 29-Apr-1994)
Ref | Expression | ||
---|---|---|---|
Assertion | difss | ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldifi | ⊢ ( 𝑥 ∈ ( 𝐴 ∖ 𝐵 ) → 𝑥 ∈ 𝐴 ) | |
2 | 1 | ssriv | ⊢ ( 𝐴 ∖ 𝐵 ) ⊆ 𝐴 |