Metamath Proof Explorer

Theorem disjiminres

Description: Disjointness condition for intersection with restriction. (Contributed by Peter Mazsa, 27-Sep-2021)

Ref Expression
Assertion disjiminres 
|- ( Disj S -> Disj ( R i^i ( S |` A ) ) )

Proof

Step Hyp Ref Expression
1 disjimres 
 |-  ( Disj S -> Disj ( S |` A ) )
2 disjimin 
 |-  ( Disj ( S |` A ) -> Disj ( R i^i ( S |` A ) ) )
3 1 2 syl 
 |-  ( Disj S -> Disj ( R i^i ( S |` A ) ) )