This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 S \to Disj (R \cap S)$

Step	Hyp	Ref	Expression
1		inss2	$⊢ R \cap S \subseteq S$
2	1	disjssi	$⊢ Disj S \to Disj (R \cap S)$