Theorem brinxp2

Description: Intersection with cross product binary relation. (Contributed by NM, 3-Mar-2007) (Revised by Mario Carneiro, 26-Apr-2015) Group conjuncts and avoid df-3an . (Revised by Peter Mazsa, 18-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		brin	|- ( C ( R i^i ( A X. B ) ) D <-> ( C R D /\ C ( A X. B ) D ) )
2		ancom	|- ( ( C R D /\ C ( A X. B ) D ) <-> ( C ( A X. B ) D /\ C R D ) )
3		brxp	|- ( C ( A X. B ) D <-> ( C e. A /\ D e. B ) )
4	3	anbi1i	|- ( ( C ( A X. B ) D /\ C R D ) <-> ( ( C e. A /\ D e. B ) /\ C R D ) )
5	1 2 4	3bitri	|- ( C ( R i^i ( A X. B ) ) D <-> ( ( C e. A /\ D e. B ) /\ C R D ) )