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 ) ) )