Description: A subset of a difference does not intersect the subtrahend. (Contributed by Jeff Hankins, 1-Sep-2013) (Proof shortened by Mario Carneiro, 24-Aug-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ssdifin0 | ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) = ∅ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrin | ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) ⊆ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) ) | |
2 | incom | ⊢ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) = ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) | |
3 | disjdif | ⊢ ( 𝐶 ∩ ( 𝐵 ∖ 𝐶 ) ) = ∅ | |
4 | 2 3 | eqtri | ⊢ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) = ∅ |
5 | sseq0 | ⊢ ( ( ( 𝐴 ∩ 𝐶 ) ⊆ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) ∧ ( ( 𝐵 ∖ 𝐶 ) ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) = ∅ ) | |
6 | 1 4 5 | sylancl | ⊢ ( 𝐴 ⊆ ( 𝐵 ∖ 𝐶 ) → ( 𝐴 ∩ 𝐶 ) = ∅ ) |