Metamath Proof Explorer

Theorem relinxp

Description: Intersection with a Cartesian product is a relation. (Contributed by Peter Mazsa, 4-Mar-2019)

Ref Expression
Assertion relinxp 
|- Rel ( R i^i ( A X. B ) )

Proof

Step Hyp Ref Expression
1 relxp 
 |-  Rel ( A X. B )
2 relin2 
 |-  ( Rel ( A X. B ) -> Rel ( R i^i ( A X. B ) ) )
3 1 2 ax-mp 
 |-  Rel ( R i^i ( A X. B ) )