Metamath Proof Explorer


Theorem inxp2

Description: Intersection with a Cartesian product. (Contributed by Peter Mazsa, 18-Jul-2019)

Ref Expression
Assertion inxp2 R A × B = x y | x A y B x R y

Proof

Step Hyp Ref Expression
1 relinxp Rel R A × B
2 dfrel4v Rel R A × B R A × B = x y | x R A × B y
3 1 2 mpbi R A × B = x y | x R A × B y
4 brinxp2 x R A × B y x A y B x R y
5 4 opabbii x y | x R A × B y = x y | x A y B x R y
6 3 5 eqtri R A × B = x y | x A y B x R y