This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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