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 𝑆 → Disj ( 𝑅 ∩ 𝑆 ) )

Proof

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