Metamath Proof Explorer


Theorem brcnvin

Description: Intersection with a converse, binary relation. (Contributed by Peter Mazsa, 24-Mar-2024)

Ref Expression
Assertion brcnvin
|- ( ( A e. V /\ B e. W ) -> ( A ( R i^i `' S ) B <-> ( A R B /\ B S A ) ) )

Proof

Step Hyp Ref Expression
1 brin
 |-  ( A ( R i^i `' S ) B <-> ( A R B /\ A `' S B ) )
2 brcnvg
 |-  ( ( A e. V /\ B e. W ) -> ( A `' S B <-> B S A ) )
3 2 anbi2d
 |-  ( ( A e. V /\ B e. W ) -> ( ( A R B /\ A `' S B ) <-> ( A R B /\ B S A ) ) )
4 1 3 bitrid
 |-  ( ( A e. V /\ B e. W ) -> ( A ( R i^i `' S ) B <-> ( A R B /\ B S A ) ) )