Theorem opelinxp

Description: Ordered pair element in an intersection with Cartesian product. (Contributed by Peter Mazsa, 21-Jul-2019)

	Ref	Expression
Assertion	opelinxp	|- ( <. C , D >. e. ( R i^i ( A X. B ) ) <-> ( ( C e. A /\ D e. B ) /\ <. C , D >. e. R ) )

Proof

Step	Hyp	Ref	Expression
1		brinxp2	|- ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) )
2		df-br	|- ( C ( R i^i ( A X. B ) ) D <-> <. C , D >. e. ( R i^i ( A X. B ) ) )
3		df-br	|- ( C R D <-> <. C , D >. e. R )
4	3	anbi2i	|- ( ( ( C e. A /\ D e. B ) /\ C R D ) <-> ( ( C e. A /\ D e. B ) /\ <. C , D >. e. R ) )
5	1 2 4	3bitr3i	|- ( <. C , D >. e. ( R i^i ( A X. B ) ) <-> ( ( C e. A /\ D e. B ) /\ <. C , D >. e. R ) )