Theorem brin3

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

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

Proof

Step	Hyp	Ref	Expression
1		brin2	|- ( ( A e. V /\ B e. W ) -> ( A ( R i^i S ) B <-> A ( R |X. S ) <. B , B >. ) )
2		opidg	|- ( B e. W -> <. B , B >. = { { B } } )
3	2	adantl	|- ( ( A e. V /\ B e. W ) -> <. B , B >. = { { B } } )
4	3	breq2d	|- ( ( A e. V /\ B e. W ) -> ( A ( R |X. S ) <. B , B >. <-> A ( R |X. S ) { { B } } ) )
5	1 4	bitrd	|- ( ( A e. V /\ B e. W ) -> ( A ( R i^i S ) B <-> A ( R |X. S ) { { B } } ) )