Theorem ssdisj

Description: Intersection with a subclass of a disjoint class. (Contributed by FL, 24-Jan-2007) (Proof shortened by JJ, 14-Jul-2021)

	Ref	Expression
Assertion	ssdisj	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ssrin	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∩ 𝐶 ) ⊆ ( 𝐵 ∩ 𝐶 ) )
2		eqimss	⊢ ( ( 𝐵 ∩ 𝐶 ) = ∅ → ( 𝐵 ∩ 𝐶 ) ⊆ ∅ )
3	1 2	sylan9ss	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) ⊆ ∅ )
4		ss0	⊢ ( ( 𝐴 ∩ 𝐶 ) ⊆ ∅ → ( 𝐴 ∩ 𝐶 ) = ∅ )
5	3 4	syl	⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝐵 ∩ 𝐶 ) = ∅ ) → ( 𝐴 ∩ 𝐶 ) = ∅ )