Theorem disjimin

Description: Disjointness condition for intersection. (Contributed by Peter Mazsa, 11-Jun-2021) (Revised by Peter Mazsa, 28-Sep-2021)

	Ref	Expression
Assertion	disjimin	⊢ ( Disj 𝑆 → Disj ( 𝑅 ∩ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		inss2	⊢ ( 𝑅 ∩ 𝑆 ) ⊆ 𝑆
2	1	disjssi	⊢ ( Disj 𝑆 → Disj ( 𝑅 ∩ 𝑆 ) )