Theorem ssdisjdr

Description: Subset preserves disjointness. Deduction form of ssdisj . Alternatively this could be proved with ineqcom in tandem with ssdisjd . (Contributed by Zhi Wang, 7-Sep-2024)

	Ref	Expression
Hypotheses	ssdisjd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	ssdisjdr.2	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐵 ) = ∅ )
Assertion	ssdisjdr	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐴 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		ssdisjd.1	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2		ssdisjdr.2	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐵 ) = ∅ )
3		sslin	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐶 ∩ 𝐴 ) ⊆ ( 𝐶 ∩ 𝐵 ) )
4	1 3	syl	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐴 ) ⊆ ( 𝐶 ∩ 𝐵 ) )
5		sseq0	⊢ ( ( ( 𝐶 ∩ 𝐴 ) ⊆ ( 𝐶 ∩ 𝐵 ) ∧ ( 𝐶 ∩ 𝐵 ) = ∅ ) → ( 𝐶 ∩ 𝐴 ) = ∅ )
6	4 2 5	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∩ 𝐴 ) = ∅ )