Metamath Proof Explorer

Theorem disjimxrnres

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

Ref Expression
Assertion disjimxrnres 
|- ( Disj S -> Disj ( R |X. ( S |` A ) ) )

Proof

Step Hyp Ref Expression
1 disjimres 
 |-  ( Disj S -> Disj ( S |` A ) )
2 disjimxrn 
 |-  ( Disj ( S |` A ) -> Disj ( R |X. ( S |` A ) ) )
3 1 2 syl 
 |-  ( Disj S -> Disj ( R |X. ( S |` A ) ) )