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 -> Disj ( R i^i S ) )

Proof

Step Hyp Ref Expression
1 inss2 
 |-  ( R i^i S ) C_ S
2 1 disjssi 
 |-  ( Disj S -> Disj ( R i^i S ) )