Theorem inxp2

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

	Ref	Expression
Assertion	inxp2	|- ( R i^i ( A X. B ) ) = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ x R y ) }

Proof

Step	Hyp	Ref	Expression
1		relinxp	|- Rel ( R i^i ( A X. B ) )
2		dfrel4v	|- ( Rel ( R i^i ( A X. B ) ) <-> ( R i^i ( A X. B ) ) = { <. x , y >. | x ( R i^i ( A X. B ) ) y } )
3	1 2	mpbi	|- ( R i^i ( A X. B ) ) = { <. x , y >. | x ( R i^i ( A X. B ) ) y }
4		brinxp2	|- ( x ( R i^i ( A X. B ) ) y <-> ( ( x e. A /\ y e. B ) /\ x R y ) )
5	4	opabbii	|- { <. x , y >. | x ( R i^i ( A X. B ) ) y } = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ x R y ) }
6	3 5	eqtri	|- ( R i^i ( A X. B ) ) = { <. x , y >. | ( ( x e. A /\ y e. B ) /\ x R y ) }