Theorem brin2

Description: Binary relation on an intersection is a special case of binary relation on range Cartesian product. (Contributed by Peter Mazsa, 21-Aug-2021)

	Ref	Expression
Assertion	brin2	|- ( ( A e. V /\ B e. W ) -> ( A ( R i^i S ) B <-> A ( R |X. S ) <. B , B >. ) )

Proof

Step	Hyp	Ref	Expression
1		brin	|- ( A ( R i^i S ) B <-> ( A R B /\ A S B ) )
2		brxrn	|- ( ( A e. V /\ B e. W /\ B e. W ) -> ( A ( R |X. S ) <. B , B >. <-> ( A R B /\ A S B ) ) )
3	2	3anidm23	|- ( ( A e. V /\ B e. W ) -> ( A ( R |X. S ) <. B , B >. <-> ( A R B /\ A S B ) ) )
4	1 3	bitr4id	|- ( ( A e. V /\ B e. W ) -> ( A ( R i^i S ) B <-> A ( R |X. S ) <. B , B >. ) )